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

Instituce: Fakulty UK (VŠKP) (web)
Informace o dostupnosti dokumentu: Dostupné v digitálním repozitáři UK.
Původní záznam: http://hdl.handle.net/20.500.11956/92888

Trvalý odkaz NUŠL: http://www.nusl.cz/ntk/nusl-369534


Záznam je zařazen do těchto sbírek:
Školství > Veřejné vysoké školy > Univerzita Karlova > Fakulty UK (VŠKP)
Vysokoškolské kvalifikační práce > Disertační práce
 Záznam vytvořen dne 2017-11-08, naposledy upraven 2022-03-04.


Není přiložen dokument
  • Exportovat ve formátu DC, NUŠL, RIS
  • Sdílet