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

Advanced Methods for Automatic Verification of Infinite-state Systems

Czech title:Pokročilé techniky automatické verifikace nekonečně stavových systémů
Reseach leader:Vojnar Tomáš
Team leaders:Habermehl Peter (UPAR7)
Team members:Bouajjani Ahmed (UPAR7), Češka Milan, Holík Lukáš, Rogalewicz Adam, Smrčka Aleš, Touili Tayssir (LIAFA UP7/CNRS)
Agency:Barrande - Czech-French programme of integrated actions
Code:MEB 020840
Start:2008-02-20
End:2009-12-31
Keywords:formal verification, infinite-state systems, model checking
Annotation:
One of the currently most studied approaches to formal verification is model checking, which is attractive by its high degree of automation and at the same time a high degree of precision. Most of the research on model checking has so-far concentrated on systems with possibly large, but finite state spaces. However, many systems that one encounters in practice are infinite-state. Infinity can arise due to dealing with various kinds of unbounded data structures such as push-down stacks needed for dealing with recursive procedures, FIFO (and other kinds) of communication channels or waiting queues, unrestricted counters (or integer variables), dynamic linked data structures (such as lists or trees). Yet another source of infinity is then dealing with various kinds of parameters (such as the maximum value of some variable, the maximum length of a queue, or the number of processes in a system). Consequently, techniques applying model checking in the area of infinite-state systems have begun to appear as well.

Among the most successful approaches to infinite-state model checking that have been proposed so-far, an important role is played by symbolic methods based on using various formalisms (such as logics, automata, grammars, etc.) for a finite representation of infinite sets of reachable states. Members of the project team have significantly contributed to the research in this area by several internationally recognised and cited results including original methods of symbolic, automata-based model checking combined with automated abstraction (the so-called abstract regular model checking---ARMC, methods based on automatic inference (learning) of regular languages representing sets of reachable states from their samples, and a series of methods for verifying programs manipulating dynamic linked data structures (using ARMC, automated detection of repeated memory patterns, or different types of extended automata with constraints).

The efficiency of the current methods of model checking of infinite-state systems is, however, still far from a broad practical applicability, and the classes of systems and their properties of interest on which these methods are applicable are also restricted. Therefore, the goal of the project is to contribute to the research on methods of model checking of infinite-state systems in order to significantly lift their current restrictions both in terms of efficiency as well as generality.

In particular, in order to contribute to an increased efficiency of the existing symbolic model checking approaches for infinite-state systems, the project will, e.g., consider development of symbolic model checking approaches based on non-deterministic automata (avoiding the determinisation step that turns out to be one of the most expensive steps in the current approaches). This implies a need of development of all the needed automata operations (such as emptiness checking, inclusion checking, minimisation, abstraction) for different kinds non-deterministic automata (word automata, tree automata, etc.). In the area of increasing the generality of the existing approaches, the project will consider both dealing with more general systems (e.g., programs with unrestricted dynamic linked data structures and integer variables) as well as dealing with more complex properties to be checked (such as termination or liveness properties). In order to do so, the project will examine various extensions of the current automata and logics (e.g., combining various classes of automata and logics describing in a qualitative way the structure of system configurations with various numerical constraints) and also of the procedures of dealing with them (including advanced decision procedures over logics, new abstraction and inference methods over automata, etc.).

Products

2009FLATA, software, 2009
Authors: Konečný Filip, Vojnar Tomáš, Bozga Marius, Iosif Radu

Publications

2010HABERMEHL Peter, IOSIF Radu and VOJNAR Tomáš. Automata-based Verification of Programs with Tree Updates. Acta Informatica. 2010, vol. 47, no. 1, pp. 1-31. ISSN 0001-5903.
2009ABDULLA Parosh A., BOUAJJANI Ahmed, HOLÍK Lukáš, KAATI Lisa and VOJNAR Tomáš. Composed Bisimulation for Tree Automata. International Journal of Foundations of Computer Science. 2009, vol. 20, no. 4, pp. 685-700. ISSN 0129-0541.
 ABDULLA Parosh A., HOLÍK Lukáš, CHEN Yu-Fang and VOJNAR Tomáš. Mediating for Reduction (On Minimizing Alternating Büchi Automata). Brno: Faculty of Information Technology BUT, 2009.
 ABDULLA Parosh A., HOLÍK Lukáš, CHEN Yu-Fang and VOJNAR Tomáš. Mediating for Reduction (On Minimizing Alternating Büchi Automata). FIT-TR-2009-02, Brno, 2009.
 ABDULLA Parosh A., HOLÍK Lukáš, CHEN Yu-Fang and VOJNAR Tomáš. Mediating for Reduction (On Minimizing Alternating Büchi Automata). In: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (2009). Wadern: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2009, pp. 1-12. ISBN 978-3-939897-13-2.
 ABDULLA Parosh A., HOLÍK Lukáš, KAATI Lisa and VOJNAR Tomáš. A Uniform (Bi-)Simulation-Based Framework for Reducing Tree Automata. Electronic Notes in Theoretical Computer Science. 2009, vol. 2009, no. 251, pp. 27-48. ISSN 1571-0661.
 BOZGA Marius, HABERMEHL Peter, IOSIF Radu, KONEČNÝ Filip and VOJNAR Tomáš. Automatic Verification of Integer Array Programs. TR-2009-2, Grenoble: VERIMAG, 2009.
 BOZGA Marius, HABERMEHL Peter, IOSIF Radu, KONEČNÝ Filip and VOJNAR Tomáš. Automatic Verification of Integer Array Programs. In: Computer Aided Verification. Berlin: Springer Verlag, 2009, pp. 157-172. ISBN 978-3-642-02657-7.
 HOLÍK Lukáš and ŠIMÁČEK Jiří. Optimizing an LTS-Simulation Algorithm. FIT-TR-2009-03, Brno, 2009.
 HOLÍK Lukáš and ŠIMÁČEK Jiří. Optimizing an LTS-Simulation Algorithm. In: 5th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science. Znojmo: Faculty of Informatics MU, 2009, pp. 93-101. ISBN 978-3-939897-15-6.
 IOSIF Radu and ROGALEWICZ Adam. Automata-Based Termination Proofs. In: Implementation and Application of Automata. Berlin: Springer Verlag, 2009, pp. 165-177. ISBN 978-3-642-02978-3.
2008ABDULLA Parosh A., BOUAJJANI Ahmed, HOLÍK Lukáš, KAATI Lisa and VOJNAR Tomáš. Composed Bisimulation for Tree Automata. In: Implementation and Application of Automata. Berlin: Springer Verlag, 2008, pp. 212-222. ISBN 978-3-540-70843-8.
 ABDULLA Parosh A., HOLÍK Lukáš, KAATI Lisa and VOJNAR Tomáš. A Uniform (Bi-)Simulation-Based Framework for Reducing Tree Automata. In: 4th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science. Brno: Faculty of Informatics MU, 2008, pp. 3-11. ISBN 978-80-7355-082-0.
 BOUAJJANI Ahmed, HABERMEHL Peter, HOLÍK Lukáš, TOUILI Tayssir and VOJNAR Tomáš. Antichain-based Universality and Inclusion Testing over Nondeterministic Finite Tree Automata. FIT-TR-2008-007, Brno: Faculty of Information Technology BUT, 2008.
 BOUAJJANI Ahmed, HABERMEHL Peter, HOLÍK Lukáš, TOUILI Tayssir and VOJNAR Tomáš. Antichain-based Universality and Inclusion Testing over Nondeterministic Finite Tree Automata. In: Implementation and Application of Automata. Berlin: Springer Verlag, 2008, pp. 57-67. ISBN 978-3-540-70843-8.
 HABERMEHL Peter and VOJNAR Tomáš, ed. Proceedings of 10th International Workshop on Verification of Infinite-State Systems - INFINITY'08. Toronto: Faculty of Information Technology BUT, 2008. ISBN 978-80-214-3697-8.
 HABERMEHL Peter, IOSIF Radu and VOJNAR Tomáš. A Logic of Singly Indexed Arrays. TR-2008-9, Grenoble: VERIMAG, 2008.
 HABERMEHL Peter, IOSIF Radu and VOJNAR Tomáš. What else is decidable about integer arrays?. TR-2007-8, Grenoble: VERIMAG, 2008.
 HABERMEHL Peter, IOSIF Radu and VOJNAR Tomáš. A Logic of Singly Indexed Arrays. In: Logic for Programming, Artificial Intelligence and Reasoning. Berlin: Springer Verlag, 2008, pp. 558-573. ISBN 978-3-540-89438-4.

Your IPv4 address: 54.91.171.137
Switch to IPv6 connection

DNSSEC [dnssec]