|
|
Verifikace programů s ukazateli založená na detekci vzorů
Kubíček, Jan ; Erlebach, Pavel (oponent) ; Vojnar, Tomáš (vedoucí práce)
Tato práce navazuje na výsledky studií v oblasti verifikace nekonečně stavových systémů. Konkrétně se jedná o oblast abstraktního model checkingu. Seznámili jsme se s metodou založenou na abstrakci paměťové konfigurace pomocí paměťových vzorů. Tato metoda byla navržena pro verifikaci programů pracujících s dynamickými paměťovými strukturami jako například seznamy. Na dynamické paměťové struktury je nahlíženo jako na orientované grafy. Verifikace na základě paměťových vzorů abstrahuje obecně libovolné množství vytvořených uzlů do jednoho sumarizovaného uzlu. Tím se dosáhne reprezentace obecně neukončeného grafu konečným zápisem. Poté je možno efektivně provést verifikaci nad tímto abstrahovaným grafem. V naší práci se zabýváme tvorbou modelu pro nástroj implementující verifikaci na základě paměťových vzorů. Model programu je vytvořen z podmnožiny jazyka C. Hlavním přínosem práce je automatizace tvorby modelu pro verifikaci a tím dosáhnutí úplné automatizovanosti procesu verifikace. Je tak možné verifikovat programy napsané v běžném programovacím jazyce. V této práci je diskutována syntaxe vstupního jazyka i implementační detaily překladu.
|
|
|
Automata in Decision Procedures and Performance Analysis
Fiedor, Tomáš ; Barnat, Jiří (oponent) ; Radu, Iosif (oponent) ; Vojnar, Tomáš (vedoucí práce)
This thesis focuses on improving the state of the art of automata-based formal analysis and verification techniques for systems with an infinite state space. In the first part of the thesis, we develop two efficient decision procedures for the WS1S logic, both of them exploiting the correspondence between formulae of WS1S logic and finite automata. We start by proposing a novel antichain-based decision procedure which is, however, limited to formulae in the prenex normal form. Later, we generalize the approach to arbitrary formulae by defining the so-called language terms and constructing an on-the-fly procedure dealing with the terms using lazy techniques. In order to achieve an efficient implementation, we propose numerous optimizations (some of these optimization are not limited to our approaches only). We evaluated both our methods with other recent state-of-the art tools. The achieved results are encouraging and show we can extend the usage of WS1S to wider classes of formulae. The second part of the thesis focuses on resource bounds analysis of heap-manipulating programs. We propose a new class of shape norms based on lengths of paths between distinct points in the heap, which we derive automatically from the analysed program. For this class of norms, we introduce a calculus capable of precisely inferring changes of the analysed norms and use it to generate a corresponding integer representation of an input program followed by dedicated state-of-the art resource bounds analysis. We implemented our approach over the shape analysis based on forest-automata, implemented in the Forester tool, and using a well-established resource bounds analyser, implemented in the Loopus tool. In our experimental evaluation, we show that we indeed obtained a powerful analyser that is able to handle some showcase examples that were never analysed fully automatically before.
|
|
|
Automata in Decision Procedures and Performance Analysis
Fiedor, Tomáš ; Barnat, Jiří (oponent) ; Radu, Iosif (oponent) ; Vojnar, Tomáš (vedoucí práce)
This thesis focuses on improving the state of the art of automata-based formal analysis and verification techniques for systems with an infinite state space. In the first part of the thesis, we develop two efficient decision procedures for the WS1S logic, both of them exploiting the correspondence between formulae of WS1S logic and finite automata. We start by proposing a novel antichain-based decision procedure which is, however, limited to formulae in the prenex normal form. Later, we generalize the approach to arbitrary formulae by defining the so-called language terms and constructing an on-the-fly procedure dealing with the terms using lazy techniques. In order to achieve an efficient implementation, we propose numerous optimizations (some of these optimization are not limited to our approaches only). We evaluated both our methods with other recent state-of-the art tools. The achieved results are encouraging and show we can extend the usage of WS1S to wider classes of formulae. The second part of the thesis focuses on resource bounds analysis of heap-manipulating programs. We propose a new class of shape norms based on lengths of paths between distinct points in the heap, which we derive automatically from the analysed program. For this class of norms, we introduce a calculus capable of precisely inferring changes of the analysed norms and use it to generate a corresponding integer representation of an input program followed by dedicated state-of-the art resource bounds analysis. We implemented our approach over the shape analysis based on forest-automata, implemented in the Forester tool, and using a well-established resource bounds analyser, implemented in the Loopus tool. In our experimental evaluation, we show that we indeed obtained a powerful analyser that is able to handle some showcase examples that were never analysed fully automatically before.
|
|
|
Verifikace programů s ukazateli založená na detekci vzorů
Kubíček, Jan ; Erlebach, Pavel (oponent) ; Vojnar, Tomáš (vedoucí práce)
Tato práce navazuje na výsledky studií v oblasti verifikace nekonečně stavových systémů. Konkrétně se jedná o oblast abstraktního model checkingu. Seznámili jsme se s metodou založenou na abstrakci paměťové konfigurace pomocí paměťových vzorů. Tato metoda byla navržena pro verifikaci programů pracujících s dynamickými paměťovými strukturami jako například seznamy. Na dynamické paměťové struktury je nahlíženo jako na orientované grafy. Verifikace na základě paměťových vzorů abstrahuje obecně libovolné množství vytvořených uzlů do jednoho sumarizovaného uzlu. Tím se dosáhne reprezentace obecně neukončeného grafu konečným zápisem. Poté je možno efektivně provést verifikaci nad tímto abstrahovaným grafem. V naší práci se zabýváme tvorbou modelu pro nástroj implementující verifikaci na základě paměťových vzorů. Model programu je vytvořen z podmnožiny jazyka C. Hlavním přínosem práce je automatizace tvorby modelu pro verifikaci a tím dosáhnutí úplné automatizovanosti procesu verifikace. Je tak možné verifikovat programy napsané v běžném programovacím jazyce. V této práci je diskutována syntaxe vstupního jazyka i implementační detaily překladu.
|
host ::
RSS.