Szoftver helyességének ellenőrzése formális módszerekkel

Tanszéki konzulens: 
A doktorandusz fényképe
doktorandusz
Szoba: IL405
Tel.:
+36 1 463-
Email: bajczi (*) mit * bme * hu

A kiírás adatai

A téma státusza: 
Aktív (aktuális, lehet rá jelentkezni)
Kiírás éve: 
2023
A kiírás jellege: 
önálló labor, szakdolgozat/diplomaterv

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.

Kapcsolódó tantárgyak: 
Formális módszerek
© 2010-2024 BME MIT | Hibajelentés | Használati útmutató