Project Details

Techniques avancées pour la vérification de systémes a nombre d'états infini

Project Period: 20. 2. 2008 - 31. 12. 2009

Project Type: grant

Code: MEB 020840

Agency: Barrande - Czech-French programme of integrated actions

Program:

Type
grant
Keywords

formal verification, infinite-state systems, model checking

Abstract

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.).

Team members
Vojnar Tomáš, prof. Ing., Ph.D. (UITS FIT VUT) , research leader
Habermehl Peter (UPAR7) , team leader
Bouajjani Ahmed (UPAR7)
Češka Milan, prof. RNDr., CSc. (UITS FIT VUT)
Holík Lukáš, doc. Mgr., Ph.D. (UITS FIT VUT)
Rogalewicz Adam, doc. Mgr., Ph.D. (UITS FIT VUT)
Smrčka Aleš, Ing., Ph.D. (UITS FIT VUT)
Touili Tayssir (LIAFA UP7/CNRS)
Publications

2010

  • HABERMEHL Peter, IOSIF Radu and VOJNAR Tomáš. Automata-based Verification of Programs with Tree Updates. Acta Informatica, vol. 47, no. 1, 2010, pp. 1-31. ISSN 0001-5903. Detail

2009

  • 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, vol. 2009, no. 251, pp. 27-48. ISSN 1571-0661. Detail
  • IOSIF Radu and ROGALEWICZ Adam. Automata-Based Termination Proofs. In: Implementation and Application of Automata. Lecture Notes in Computer Science, vol. 5642. Berlin: Springer Verlag, 2009, pp. 165-177. ISBN 978-3-642-02978-3. Detail
  • BOZGA Marius, HABERMEHL Peter, IOSIF Radu, KONEČNÝ Filip and VOJNAR Tomáš. Automatic Verification of Integer Array Programs. In: Computer Aided Verification. Lecture Notes in Computer Science, vol. 5643. Berlin: Springer Verlag, 2009, pp. 157-172. ISBN 978-3-642-02657-7. Detail
  • BOZGA Marius, HABERMEHL Peter, IOSIF Radu, KONEČNÝ Filip and VOJNAR Tomáš. Automatic Verification of Integer Array Programs. TR-2009-2, Grenoble: VERIMAG, 2009. Detail
  • ABDULLA Parosh A., BOUAJJANI Ahmed, HOLÍK Lukáš, KAATI Lisa and VOJNAR Tomáš. Composed Bisimulation for Tree Automata. International Journal of Foundations of Computer Science, vol. 20, no. 4, 2009, pp. 685-700. ISSN 0129-0541. Detail
  • 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. Detail
  • 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. Detail
  • 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). LIPIcs, sv. 4. Wadern: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2009, pp. 1-12. ISBN 978-3-939897-13-2. Detail
  • HOLÍK Lukáš and ŠIMÁČEK Jiří. Optimizing an LTS-Simulation Algorithm. FIT-TR-2009-03, Brno, 2009. Detail
  • 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. Detail

2008

  • HABERMEHL Peter, IOSIF Radu and VOJNAR Tomáš. A Logic of Singly Indexed Arrays. In: Logic for Programming, Artificial Intelligence and Reasoning. Lecture Notes in Computer Science, vol. 5330. Berlin: Springer Verlag, 2008, pp. 558-573. ISBN 978-3-540-89438-4. Detail
  • HABERMEHL Peter, IOSIF Radu and VOJNAR Tomáš. A Logic of Singly Indexed Arrays. TR-2008-9, Grenoble: VERIMAG, 2008. Detail
  • 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. Detail
  • 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. Lecture Notes in Computer Science, vol. 5148. Berlin: Springer Verlag, 2008, pp. 57-67. ISBN 978-3-540-70843-8. Detail
  • 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. Detail
  • ABDULLA Parosh A., BOUAJJANI Ahmed, HOLÍK Lukáš, KAATI Lisa and VOJNAR Tomáš. Composed Bisimulation for Tree Automata. In: Implementation and Application of Automata. Lecture Notes in Computer Science, vol. 5148. Berlin: Springer Verlag, 2008, pp. 212-222. ISBN 978-3-540-70843-8. Detail
  • 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. Detail
  • HABERMEHL Peter, IOSIF Radu and VOJNAR Tomáš. What else is decidable about integer arrays?. TR-2007-8, Grenoble: VERIMAG, 2008. Detail
Products

2009

  • FLATA, software, 2009
    Authors: Konečný Filip, Vojnar Tomáš, Bozga Marius, Iosif Radu Detail
Back to top