Ph.D. Thesis
| Author: | Ondřej Lengál |
| Title: | Automata in Infinite-State Formal Verification |
| Advisor: | prof. Ing. Tomáš Vojnar, Ph.D. |
| Affiliation: | Faculty of Information Technology, Brno University of Technology |
| Defense date: | 2 July 2015 |
Abstract (English)
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 dynamic data 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.
Abstract (Czech)
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.
Attachments
| Thesis: | lengal-thesis.pdf |
| Thesis statement: | lengal-statement.pdf |
| Thesis slides: | lengal-slides.pdf |
Publications
- P.A. Abdulla, L. Holik, B. Jonsson, O. Lengal, C.Q. Trinh, and T. Vojnar. Verification of Heap Manipulating Programs with Ordered Data by Extended Forest Automata. Acta Informatica. Springer-Verlag.
- T. Fiedor, L. Holik, O. Lengal, and T. Vojnar. Nested Antichains for WS1S. In Proc. of 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems — TACAS'15, London, United Kingdom, volume 9035 of LNCS, pages 658--674, 2015. Springer-Verlag.
- L. Holik, M. Hruska, O. Lengal, A. Rogalewicz, J. Simacek, and T. Vojnar. Forester: Shape Analysis Using Tree Automata (Competition Contribution). In Proc. of 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems — TACAS'15, London, United Kingdom, volume 9035 of LNCS, pages 431--434, 2015. Springer-Verlag.
- C. Enea, O. Lengal, M. Sighireanu, and T. Vojnar. Compositional Entailment Checking for a Fragment of Separation Logic. In Proc. of 12th Asian Symposium on Programming Languages and Systems — APLAS'14, Singapore, Singapore, volume 8858 of LNCS, pages 314--333, 2014. Springer-Verlag.
- P.A. Abdulla, L. Holik, B. Jonsson, O. Lengal, C.Q. Trinh, and T. Vojnar. Verification of Heap Manipulating Programs with Ordered Data by Extended Forest Automata. In Proc. of 11th International Symposium on Automated Technology for Verification and Analysis — ATVA'13, Hanoi, Vietnam, volume 8172 of LNCS, pages 224--239, 2013. Springer-Verlag.
- L. Holik, O. Lengal, A. Rogalewicz, J. Simacek, and T. Vojnar. Fully Automated Shape Analysis Based on Forest Automata. In Proc. of 25th International Conference on Computer Aided Verification — CAV'13, Saint Petersburg, Russia, volume 8044 of LNCS, pages 740--755, 2013. Springer-Verlag.
- O. Lengal, J. Simacek, and T. Vojnar. VATA: A Library for Efficient Manipulation of Non-Deterministic Tree Automata. In Proc. of 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems — TACAS'12, Tallinn, Estonia, volume 7214 of LNCS, pages 79--94, 2012. Springer-Verlag.
- L. Holik, O. Lengal, J. Simacek, and T. Vojnar. Efficient Inclusion Checking on Explicit and Semi-Symbolic Tree Automata. In Proc. of 9th International Symposium on Automated Technology for Verification and Analysis — ATVA'11, Taipei, Taiwan, volume 6996 of LNCS, pages 243--258, 2011. Springer-Verlag.