Název:
Reprezentace stavů programu
Překlad názvu:
Efficient Representation of Program States
Autoři:
Jančík, Pavel ; Kofroň, Jan (vedoucí práce) ; Gargantini, Angelo (oponent) ; Barnat, Jiří (oponent) Typ dokumentu: Disertační práce
Rok:
2017
Jazyk:
eng
Abstrakt: Při verifikaci programů se snažíme rozhodnout, zda program obsahuje či neobsahuje chyby. Základním předpokladem všech verifikačních postupů je efektivní reprezentace a manipulace se stavy programů. V této práci představujeme techniky pro nalezení nepodstatných informací ve stavech programů a pro jejich odstranění. Tato práce obsahuje redukce vhodné pro explicitní i symbolickou reprezentaci stavů. Naše postupy vhodné pro explicitní reprezentaci byly speciálně navrženy pro vícevláknové programy. Naše analýzy dokáží nalézt takové hodnoty v dynamicky alokovaných objektech, tedy na haldě, které program již nebude v následujících krocích číst. Logické formule v predikátové nebo výrokové logice jsou převažující symbolickou reprezentací množin stavů programu. Craigovy interpolanty jsou jedním z obvyklých postupů pro získání formulí s požadovanými vlastnostmi. V této práci představujeme nový způsob jejich výpočtu, který používá přiřazení proměnných pro zmenšení jejich velikosti. Pomocí přiřazení proměnných můžeme zablokovat ty cesty v programu, které nechceme, aby interpolant bral v potaz a tím zmenšit jejich velikost.
Klíčová slova:
Interpolanty; Model checking kódu; Porovnávání stavů; Verifikace software; Code model checking; Craig Interpolation; Software verification; State matching