Tanszéki konzulens: 

Bajczi Levente doktorandusz Szoba: IL405 Tel.: +36 1 463- Email: bajczi (*) mit * bme * hu

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, azzal a céllal, hogy támogassa az absztrakciós finomításon alapuló algoritmusok tervezését és értékelését különböző formalizmusok elérhetőségi elemzéséhez. A Theta fő megkülönböztető jellemzője az architektúrája, amely lehetővé teszi a magasabb szintű nyelvi front-enddel rendelkező bemeneti formalizmusok definiálását, valamint különböző absztrakt domének, interpreterek és absztrakció-finomítási stratégiák kombinálását. A Theta egyszerre szolgálhat modellellenőrző backendként, és tartalmaz kész, önálló eszközöket is.

A témakiírás a Theta keretrendszerhez kapcsolódó elméleti és gyakorlati fejlesztéseket, algoritmusok kidolgozását, implementálását és bizonyítását foglalja magában. Meglévő implementációk optimalizálását, új irányok felderítését és friss tudományos eredmények alapján algoritmus-implementálást lehet a téma keretében végezni.