Project Details

Vérification automatique de programmes avec structures de données dynamiques a pointeurs

Project Period: 1. 1. 2006 - 31. 12. 2007

Project Type: grant

Code: 2-06-27

Agency: Barrande - Czech-French programme of integrated actions

Program:

Type
grant
Keywords

formal verification, infinite-state systems, regular model checking, programs with dynamic linked data structures

Abstract

Though there have already been proposed multiple approaches to automatic formal verification (or static analysis) of programs with pointers and dynamic linked data structures, these approaches are still far from being general (i.e. covering all the different shapes of structures that one may encounter in practice), fully automatic, and at the same time efficient. The goal of the present project is thus to push the current state-of-the-art in the given area as far as possible towards obtaining techniques for automated verification of programs with dynamic linked data structures that would meet the above described criteria. The way the project intends to achieve the above goal is primarily based on a further development of the abstract regular model checking (ARMC) framework proposed by A. Boujjani, P. Habermehl, and T. Vojnar at CAV 2004.

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)
Erlebach Pavel, Ing. (UITS FIT VUT)
Holík Lukáš, doc. Mgr., Ph.D. (UITS FIT VUT)
Moro Pierre (LIAFA UP7/CNRS)
Rogalewicz Adam, doc. Mgr., Ph.D. (UITS FIT VUT)
Touili Tayssir (LIAFA UP7/CNRS)
Publications

2008

  • ABDULLA Parosh A., HOLÍK Lukáš, KAATI Lisa and VOJNAR Tomáš. A Uniform (Bi-)Simulation-Based Framework for Reducing Tree Automata. FIT-TR-2008-005, Brno, 2008. Detail
  • VOJNAR Tomáš, ČEŠKA Milan, ROGALEWICZ Adam, ERLEBACH Pavel, HOLÍK Lukáš, BOUAJJANI Ahmed, HABERMEHL Peter, TOUILI Tayssir and MORO Pierre. Automatická verifikace programů s dynamickými datovými strukturami. Inovační podnikání & transfer technologií, vol. 2008, no. 1, pp. 21-22. ISSN 1210-4612. Detail
  • ABDULLA Parosh A., BOUAJJANI Ahmed, HOLÍK Lukáš, KAATI Lisa and VOJNAR Tomáš. Computing Simulations over Tree Automata: Efficient Techniques for Reducing Tree Automata. FIT-TR-2008-001, Brno, 2008. Detail
  • HABERMEHL Peter, IOSIF Radu and VOJNAR Tomáš. What else is decidable about integer arrays?. In: Foundations of Software Science and Computation Structures. Lecture Notes in Computer Science, vol. 4962. Berlin: Springer Verlag, 2008, pp. 475-490. ISBN 978-3-540-78497-5. Detail

2007

  • HOLÍK Lukáš and ROGALEWICZ Adam. Counterexample Analysis in Abstract Regular Tree Model Checking of Complex Dynamic Data Structures. In: Third Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2007). Znojmo: Ing. Zdeněk Novotný, CSc., 2007, pp. 59-66. ISBN 978-80-7355-077-6. Detail
  • VOJNAR Tomáš. Cut-offs and Automata in Formal Verification of Infinite-State Systems. FIT Monograph 1. Brno: Faculty of Information Technology BUT, 2007. ISBN 978-80-214-3547-6. Detail
  • ČEŠKA Milan, ERLEBACH Pavel and VOJNAR Tomáš. Generalised Multi-Pattern-Based Verification of Programs with Linear Linked Structures. Formal Aspects of Computing, vol. 19, no. 3, 2007, pp. 363-374. ISSN 0934-5043. Detail
  • ČEŠKA Milan, ERLEBACH Pavel and VOJNAR Tomáš. Pattern-based Verification for Trees. In: Computer Aided Systems Theory. Lecture Notes in Computer Science, vol. 4739. Berlin: Springer Verlag, 2007, pp. 488-496. ISBN 978-3-540-75866-2. Detail
  • ČEŠKA Milan, ERLEBACH Pavel and VOJNAR Tomáš. Pattern-Based Verification for Trees. In: Computer Aided Systems Theory - EUROCAST 2007. Las Palmas de Grand Canaria: The Universidad de Las Palmas de Gran Canaria, 2007, pp. 181-182. ISBN 978-3-540-75866-2. Detail
  • HABERMEHL Peter, IOSIF Radu, ROGALEWICZ Adam and VOJNAR Tomáš. Proving Termination of Tree Manipulating Programs. In: Automated Technology for Verification and Analysis. Lecture Notes in Computer Science, vol. 4762. Berlin: Springer Verlag, 2007, pp. 145-161. ISBN 978-3-540-75595-1. Detail
  • ROGALEWICZ Adam. Verification of Programs with Complex Data Structures. Brno, 2007. ISBN 978-80-214-3548-3. Detail

2006

  • BOUAJJANI Ahmed, HABERMEHL Peter, ROGALEWICZ Adam and VOJNAR Tomáš. Abstract Regular Tree Model Checking. Electronic Notes in Theoretical Computer Science, vol. 149, no. 1, 2006, pp. 37-48. ISSN 1571-0661. Detail
  • BOUAJJANI Ahmed, HABERMEHL Peter, ROGALEWICZ Adam and VOJNAR Tomáš. Abstract Regular Tree Model Checking of Complex Dynamic Data Structures. In: Static Analysis. Lecture Notes in Computer Science, vol. 4134. Berlin: Springer Verlag, 2006, pp. 52-70. ISBN 978-3-540-37756-6. Detail
  • HABERMEHL Peter, IOSIF Radu and VOJNAR Tomáš. Automata-based Verification of Programs with Tree Updates. In: Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 3920. Berlin: Springer Verlag, 2006, pp. 350-364. ISBN 978-3-540-33056-1. Detail
Back to top