Automaty v rozhodovacích procedurách a výkonnostní analýze

Tato práce se věnuje vylepšení současného stavu formalní analýzy a verifikace založené na automatech a zaměřené na systémy s nekonečnými stavovými prostory. V první části se práce zabývá dvěma rozhodovacími procedurami pro logiku WS1S, které jsou založené na korespondenci mezi formulemi logiky WS1S a konečnými automaty. První metoda je založena na tzv. antiřetězcích, ale, je limitována pouze na formule v prenexním normálním tvaru. Následně je tento přístup zobecněn na libovolné formule, jsou zavedeny tzv. jazykové termy a na jejich základě je navržena nová procedura, která pracuje za běhu a zpracovává tyto termy "líným" způsobem. Abychom získali efektivní rozhodovací proceduru, je dále navržena sada optimalizací (přičemž některé nejsou limitovány pouze pro naše přístupy). Obě metody jsou srovnány s ostatními nástroji implementujícími různé známé rozhodovací procedury. Získané výsledky jsou povzbuzující a ukazují, že použitelnost logiky WS1S je možno rozšířit na širší třídu formulí. V druhé části se práce zabývá analýzou mezí zdrojů programů manipulujících s haldou. Je zde navržena nová třída tzv. tvarových norem založených na délkách cest mezi význačnými místy na haldě, které jsou automaticky odvozovány z analyzovaného programu. Na základě této třídy norem je dále navržen kalkul, který je schopen přesně odvodit změny odvozených normů a použít je k vygenerování odpovídající celočíselné reprezentace vstupního programu, která je následně využita pro následovanou dedikovanou analýzou mezí zdrojů. Tato metoda byla implementována nad analýzou tvaru založenou na tzv. lesních automatech, implementovanou v nástroji Forester, a dále byl použit dobře zavedený analyzátor mezí zdrojů, implementovaný v nástroji Loopus. V experimentální evaluaci bylo ukázáno, že je opravdu takto získán silný analyzátor, který je schopen odvodit meze programů, které ještě nikdy plně automatizovaně odvozené nebyly.

Grantor dc:publisher

Vysoké učení technické v Brně. Fakulta informačních technologií

Author dc:creator

• Fiedor, Tomáš

Advisor dc:contributor.advisor

• Vojnar, Tomáš

• Analýza mezí zdrojů
• analýza tvaru
• antiřetězce
• amortizovaná složitost
• binární rozhodovací diagramy
• formální analyza
• konečné automaty
• logika druhého řádu
• lesní automaty
• monadická logika
• programy manipulující s haldou
• nedeterminismus
• statická analýza
• stromové automaty
• tvarové normy
• ws1s.
• Antichains
• amortized complexity
• binary decision diagrams
• finite automata
• forest automata
• formal verification
• heap-manipulating programs
• monadic logic
• non-determinism
• resource bounds analysis
• second-order logic
• shape analysis
• shape norms
• static analysis
• tree automata

Statement dc:rights

• Standardní licenční smlouva - přístup k plnému textu bez omezení

Language dc:language.iso

en

Dc Identifier Other

128195

OAI identifier oai:identifier

oai:dspace.vut.cz:11012/196804