Szoftververifikáció során gyakran alkalmazunk logikai megoldókat alacsonyszintű logikai problémák megoldásához (például SAT- vagy SMT szolvereket). Ezeknek ugyanakkor vannak bizonyos limitációik, így bizonyos problémák megoldásához ígéretesebb eszköznek tűnnek a gráfmegoldók.

A Theta egy általános, moduláris és konfigurálható modellellenőrző keretrendszer, amelyet a Budapesti Műszaki és Gazdaságtudományi Egyetem Kritikus Rendszerek Kutatócsoportjában (BME, ftsrg) fejlesztettek ki, azonban jelenleg főként SMT szolvereket használ a különféle problémák megoldására. Szintén a kutatócsoportban fejlesztett eszköz a Refinery, amely alapvetően hatékony gráfgenerálásra (gráfokra vonatkozó kényszereket kielégítő gráfmodellek létrehozására) képes.

A témakiírás a verifikációs algoritmusok adaptálására vonatkozik, ahol a meglévő SMT-re építő megoldások kicserélése a cél gráfmegoldón alapuló megközelítésre. A téma sok elméleti elem mellett érdekes implementációs feladatokkal is kecsegtet, alapjául szolgálhat egy TDK dolgozatnak.