Detail projektu

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

Období řešení: 1. 1. 2006 - 31. 12. 2007

Typ projektu: grant

Kód: 2-06-27

Agentura: Barrande - česko-francouzský program integrovaných akcí

Program:

Typ
grant
Klíčová slova

formální verifikace, nekonečně stavové systémy, regulární model checking, programy s dynamickými datovými strukturami

Abstrakt

Přestože již bylo navrženo několik různých přístupů k automatizované verifikaci (či statické analýze) programů s dynamickými datovými strukturami provázanými ukazateli, tyto přístupy stále zůstávají daleko od toho, aby byly dostatečně obecné (tj. pokrývaly všechny podoby dynamických datových struktur, s nimiž se setkáváme v praxi), aby byly plně automatizované a aby byly současně efektivní. Cílem tohoto projektu je proto přispět co největší mírou k rozvoji současného stavu poznání v oblasti automatizované verifikace programů s dynamickými datovými strukturami směrem k navržení technik, které by lépe plnily výše uvedená kritéria. Způsob, jakým projekt zamýšlí dosáhnout výše uvedeného cíle, je založen především na rozvoji metody označované jako tzv. abstraktní regulární model checking (abstract regular model checking).

Řešitelé
Vojnar Tomáš, prof. Ing., Ph.D. (UITS FIT VUT) , hlavní řešitel
Habermehl Peter (UPAR7) , spoluřešitel
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)
Publikace

2008

  • ABDULLA Parosh A., HOLÍK Lukáš, KAATI Lisa a 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 a MORO Pierre. Automatická verifikace programů s dynamickými datovými strukturami. Inovační podnikání & transfer technologií, roč. 2008, č. 1, s. 21-22. ISSN 1210-4612. Detail
  • ABDULLA Parosh A., BOUAJJANI Ahmed, HOLÍK Lukáš, KAATI Lisa a VOJNAR Tomáš. Computing Simulations over Tree Automata: Efficient Techniques for Reducing Tree Automata. FIT-TR-2008-001, Brno, 2008. Detail
  • HABERMEHL Peter, IOSIF Radu a VOJNAR Tomáš. What else is decidable about integer arrays?. In: Foundations of Software Science and Computation Structures. Lecture Notes in Computer Science, roč. 4962. Berlin: Springer Verlag, 2008, s. 475-490. ISBN 978-3-540-78497-5. Detail

2007

  • HOLÍK Lukáš a 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, s. 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: Fakulta informačních technologií VUT v Brně, 2007. ISBN 978-80-214-3547-6. Detail
  • ČEŠKA Milan, ERLEBACH Pavel a VOJNAR Tomáš. Generalised Multi-Pattern-Based Verification of Programs with Linear Linked Structures. Formal Aspects of Computing, roč. 19, č. 3, 2007, s. 363-374. ISSN 0934-5043. Detail
  • ČEŠKA Milan, ERLEBACH Pavel a VOJNAR Tomáš. Pattern-based Verification for Trees. In: Computer Aided Systems Theory. Lecture Notes in Computer Science, roč. 4739. Berlin: Springer Verlag, 2007, s. 488-496. ISBN 978-3-540-75866-2. Detail
  • ČEŠKA Milan, ERLEBACH Pavel a VOJNAR Tomáš. Pattern-Based Verification for Trees. In: Computer Aided Systems Theory - EUROCAST 2007. Las Palmas de Grand Canaria: Universidad de Las Palmas de Gran Canaria, 2007, s. 181-182. ISBN 978-3-540-75866-2. Detail
  • HABERMEHL Peter, IOSIF Radu, ROGALEWICZ Adam a VOJNAR Tomáš. Proving Termination of Tree Manipulating Programs. In: Automated Technology for Verification and Analysis. Lecture Notes in Computer Science, roč. 4762. Berlin: Springer Verlag, 2007, s. 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 a VOJNAR Tomáš. Abstract Regular Tree Model Checking. Electronic Notes in Theoretical Computer Science, roč. 149, č. 1, 2006, s. 37-48. ISSN 1571-0661. Detail
  • BOUAJJANI Ahmed, HABERMEHL Peter, ROGALEWICZ Adam a VOJNAR Tomáš. Abstract Regular Tree Model Checking of Complex Dynamic Data Structures. In: Static Analysis. Lecture Notes in Computer Science, roč. 4134. Berlin: Springer Verlag, 2006, s. 52-70. ISBN 978-3-540-37756-6. Detail
  • HABERMEHL Peter, IOSIF Radu a 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, roč. 3920. Berlin: Springer Verlag, 2006, s. 350-364. ISBN 978-3-540-33056-1. Detail
Nahoru