Automata in Decision Procedures and Performance Analysis

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

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.

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,ws1s.

FIEDOR, Tomáš. Automata in Decision Procedures and Performance Analysis. Brno, 2020. Ph.D. Thesis. Brno University of Technology, Faculty of Information Technology. 2020-09-04. Supervised by Vojnar Tomáš. Available from: https://www.fit.vut.cz/study/phd-thesis/847/