Prof. Ing. Tomáš Vojnar, Ph.D.

Automata and Logic for Symbolic Verification of Software

Czech title:Automaty a logiky v symbolické verifikaci software
Reseach leader:Rogalewicz Adam
Team leaders:Iosif Radu
Team members:Bozga Marius (VERIMAG), Habermehl Peter (UPAR7), Konečný Filip, Šimáček Jiří, Vojnar Tomáš
Agency:Barrande - Czech-French programme of integrated actions
Code:MEB021023
Start:2010-01-01
End:2011-12-31
Keywords:formal verification, infinite-state systems, symbolic representations, automata, logics
Annotation:
Among techniques which can be used for verification of infinite-state systems, one can find approaches based on cut-offs, automated induction, or symbolic verification, which is probably the most frequent and which is also the subject of the proposed project. Symbolic verification is based on encoding infinite sets of states of the examined systems (possibly after some abstraction) in a finite way using some suitable formalism. Probably the most commonly used symbolic representations are those built on logics and automata.

The scientific goal of the proposed project is to significantly advance the state of the art in the area of symbolic logic-based and automata-based verification methods for infinite-state software, namely to increase the scalability of these approaches and to broaden the area of their applicability. To achieve this goal we plan to further improve the various individual logic-based as well as automata-based techniques, but also invest a significant amount of research into approaches combining advantages of both automata as well as logics. In the research, we will in particular concentrate on verification of programs with unbounded integers, (parametrised-size) arrays, and complex dynamic linked data structures.

Products

2010Forester: A Tool for Verification of Programs with Pointers, software, 2010
Authors: Habermehl Peter, Holík Lukáš, Rogalewicz Adam, Šimáček Jiří, Vojnar Tomáš

Publications

2012BOUAJJANI Ahmed, HABERMEHL Peter, ROGALEWICZ Adam and VOJNAR Tomáš. Abstract Regular (Tree) Model Checking. International Journal on Software Tools for Technology Transfer. 2012, vol. 14, no. 2, pp. 167-191. ISSN 1433-2779.
2011HABERMEHL Peter, HOLÍK Lukáš, ROGALEWICZ Adam, ŠIMÁČEK Jiří and VOJNAR Tomáš. Forest Automata for Verification of Heap Manipulation. FIT-TR-2011-01, Brno: Faculty of Information Technology BUT, 2011.
 HABERMEHL Peter, HOLÍK Lukáš, ROGALEWICZ Adam, ŠIMÁČEK Jiří and VOJNAR Tomáš. Forest Automata for Verification of Heap Manipulation. Lecture Notes in Computer Science. 2011, vol. 2011, no. 6806, pp. 424-440. ISSN 0302-9743.
2010BOZGA Marius, IOSIF Radu and KONEČNÝ Filip. Fast Acceleration of Ultimately Periodic Relations. In: Computer Aided Verification. Berlin: Springer Verlag, 2010, pp. 227-242. ISBN 978-3-642-14294-9.

Your IPv4 address: 54.91.171.137
Switch to IPv6 connection

DNSSEC [dnssec]