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.
| Identifer | oai:union.ndltd.org:nusl.cz/oai:invenio.nusl.cz:369534 |
| Date | January 2017 |
| Creators | Jančík, Pavel |
| Contributors | Kofroň, Jan, Gargantini, Angelo, Barnat, Jiří |
| Source Sets | Czech ETDs |
| Language | English |
| Detected Language | Unknown |
| Type | info:eu-repo/semantics/doctoralThesis |
| Rights | info:eu-repo/semantics/restrictedAccess |
Page generated in 0.002 seconds