Thesis Details
Automata in Infinite-state Formal Verification
The work presented in this thesis focuses on finite state automata over finite words and finite trees, and the use of such automata in formal verification of infinite-state systems. First, we focus on extensions of a previously introduced framework for verification of heap-manipulating programs-in particular programs with complex dynamicdata structures-based on tree automata. We propose several extensions to the framework, such as making it fully automated or extending it to consider ordering over data values. Further, we also propose novel decision procedures for two logics that are often used in formal verification: separation logic and weak monadic second order logic of one successor. These decision procedures are based on a translation of the problem into the domain of automata and subsequent manipulation in the target domain. Finally, we have also developed new approaches for efficient manipulation with tree automata, mainly for testing language inclusion and for handling automata with large alphabets, and implemented them in a library for general use. The developed algorithms are used as the key technology to make the above mentioned techniques feasible in practice.
antichains, binary decision diagrams, finite automata, heaps, language inclusion, monadic logic, nondeterminism, regular tree model checking, second-order logic, separation logic, shape analysis, simulation, tree automata, formal verification
@phdthesis{FITPT519,
author = "Ond\v{r}ej Leng\'{a}l",
type = "Ph.D. thesis",
title = "Automata in Infinite-state Formal Verification",
school = "Brno University of Technology, Faculty of Information Technology",
year = 2015,
location = "Brno, CZ",
language = "english",
url = "https://www.fit.vut.cz/study/phd-thesis/519/"
}