Absztrakt interpretáció alapú verifikáció

A számításelmélet területének egyik fontos módszere az absztrakt interpretáció (http://en.wikipedia.org/wiki/Abstract_interpretation), amely segítségével matematikai értelemben vett nehéz vagy eldönthetetlen problémákkal kapcsolatban is tudunk következtetni.

Az absztrakt interpretáció során absztrakciós módszerek segítségével próbálunk egyszerűsíteni a problémákon. Elterjedten használják program analízisre, szoftver modellelllenőrzés során vagy tradicionális modellellenőrzésre, ahol is a rendszer modelljének helyességét vizsgálják segítségével.

A hallgató feladata megismerkedni az absztrakt interpretáció eszköztárával, és az irodalom alapján Petri-hálók elérhetőségi analízisére alkalmazni azt a tanszéki fejlesztéső PetriDotNet keretrendszerben (http://petridotnet.inf.mit.bme.hu/).

A feladat során komoly matematikai eszköztárral kell megismerkedni, új tudományos eredmények elérése van lehetőség.