A modellellenőrzés egy automatizált, de formális ellenőrzési módszer, vagyis a modellellenőrző matematikai precizitással kell belássa hibák jelenlétét vagy hiányát a bemenetben (például egy C programban). Ennélfogva fontos, hogy az analízis végén az eredmény se csak "egy szavas" (van hiba vagy nincs) legyen, hanem egy tanú (witness) - ellenpélda vagy bizonyítás is tartozzon hozzá. Az ilyen tanúk külön kutatási területet jelentenek, hiszen ahhoz kell segítséget adniuk, hogy egy NP-teljes problémára (mint az adott C program helyessége) adott megoldás (vagyis a tanú) helyességét a segítségükkel utólag minél könnyebben be lehessen látni. Az eredmény belátása a tanú alapján a validáció. Sok validációs eszköz létezik és szerencsére egyre több elfogadja ugyanazt az egységes tanú formátumot. Ezt a formátumot a mi modellellenőrzőnk, a Theta is képes létrehozni, azonban több területen még nem elég jó minőségűek vagy hiányosak az adott tanúk - az ezen való javítást szeretnén hallgatókra bízni.

 

A téma előnye, hogy vannak gyakorlatibb (implementáció nagy szoftver projektben) és elméletibb (modellellenőrzés, tanúk és validáció megismerése) részei, így a hallgató érdeklődési körét figyelembe véve, személyes igényei szerint tudjuk megszabni a pontos feladatot.