Automaty v nekonečně stavové formální verifikaci
| Autor: | Lengál, Ondřej |
|---|---|
| Jazyk: | angličtina |
| Rok vydání: | 2015 |
| Předmět: |
heaps
finite automata regulární stromový model checking separační logika druhořádová logika konečný automat jazyková inkluze shape analysis binary decision diagrams monadická logika formal verification stromový automat formální verifikace binární rozhodovací diagramy regular tree model checking antiřetězce second-order logic separation logic language inclusion haldy simulace nondeterminism tree automata antichains nedeterminismus monadic logic simulation analýza tvaru |
| Druh dokumentu: | Doctoral Thesis |
| Popis: | Tato práce se zaměřuje na konečné automaty nad konečnými slovy a konečnými stromy, a použití těchto automatů při formální verifikaci nekonečně stavových systémů. Práce se nejdříve věnuje rozšíření existujícího přístupu pro verifikaci programů které manipulují s haldou (konkrétně programů s dynamickými datovými strukturami), jenž je založen na stromových automatech. V práci je navrženo několik rozšíření tohoto přístupu, jako například jeho plná automatizace či jeho rozšíření o podporu uspořádaných dat. V práci jsou popsány nové rozhodovací procedury pro dvě logiky, které jsou často používány ve formální verifikaci: pro separační logiku a pro slabou monadickou druhořádovou logiku s následníkem. Obě tyto rozhodovací procedury jsou založeny na převodu jejich problému do automatové domény a následné manipulaci v této cílové doméně. Posledním přínosem této práce je vývoj nových algoritmů k efektivní manipulaci se stromovými automaty, s důrazem na testování inkluze jazyků těchto automatů a manipulaci s automaty s velkými abecedami, a implementace těchto algoritmů v knihovně pro obecné použití. Tyto vyvinuté algoritmy jsou použity jako klíčová technologie, která umožňuje použití výše uvedených technik v praxi. |
| Databáze: | Networked Digital Library of Theses & Dissertations |
| Externí odkaz: |
|