Prof. RNDr. Milan Češka, CSc.

Advanced Methods of Automatic Verification of Parametric and Infinite-State Systems
Reseach leader:Vojnar Tomáš
Team leaders:Češka Milan
Agency:GAČR
Code:GP102/03/D211
Start:2003
End:2006
Keywords:formal verification, model checking, parametric and infinite state systems, concurrent systems
Annotation:
A constant growth in the complexity of computerized systems together with increasing demands on their reliability have currently lead to a strong interest in development of  automated methods and tools for rigorous verification of correctness of such systems. Systems that attract a special attention include protocols of computer and telecommunication networks, concurrent software of control and operating systems, hardware communication protocols, etc. While many relatively efficient verification methods have been proposed for the case the considered systems have a finite state space, automatic verification of infinite-state and parametric systems is significantly less developed. Many practically important systems of this kind are not covered by any automatic verification methods, or the available methods are not very efficient. Based on experience of the applicant with current capabilities and restrictions of such methods, the proposed project aims at their further development towards higher efficiency and broader applicability. A special attention will be devoted to methods of symbolic verification based on using automata and transducers for handling sets of states. Possibilities of using new types of automata together with new techniques for efficient manipulation of the current as well as newly considered types of automata will be examined. Besides the mentioned methods of symbolic verification, methods based on cut-offs and automated abstraction will be explored too. The goal of the project is not only a theoretical research, but also a prototype implementation of at least the most promising approaches out of the proposed ones.

Publications

2013Novosad Petr, Češka Milan: Algorithm for Computing Unfoldings of Unbounded Hybrid Petri Nets, In: Proc. of Computer Aided System Theory 2013, Universidad de Las Palmas de Gran Canaria, ES, IUCTC, 2013, p. 244-245, ISBN 84-695-6971-6
2007Češka Milan, Erlebach Pavel, Vojnar Tomáš: Generalised Multi-Pattern-Based Verification of Programs with Linear Linked Structures, In: Formal Aspects of Computing, Vol. 19, No. 3, 2007, London, GB, p. 363-374, ISSN 0934-5043
 Rogalewicz Adam: Verification of Programs with Complex Data Structures, Brno, CZ, 2007, p. 122, ISBN 978-80-214-3548-3
 Vojnar Tomáš: Cut-offs and Automata in Formal Verification of Infinite-State Systems, Brno, CZ, FIT VUT, 2007, p. 189, ISBN 978-80-214-3547-6
2006Bouajjani Ahmed, Habermehl Peter, Rogalewicz Adam, Vojnar Tomáš: Abstract Regular Tree Model Checking of Complex Dynamic Data Structures, In: Static Analysis, Berlin, DE, Springer, 2006, p. 52-70, ISBN 978-3-540-37756-6
 Bouajjani Ahmed, Habermehl Peter, Rogalewicz Adam, Vojnar Tomáš: Abstract Regular Tree Model Checking, In: ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, Vol. 149, No. 1, 2006, US, p. 37-48, ISSN 1571-0661
 Češka Milan, Erlebach Pavel, Vojnar Tomáš: Pattern-Based Verification of Programs with Extended Linear Linked Data Structures, In: ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, Vol. 2006, No. 145, US, p. 113-130, ISSN 1571-0661
 Habermehl Peter, Iosif Radu, Vojnar Tomáš: Automata-based Verification of Programs with Tree Updates, In: Tools and Algorithms for the Construction and Analysis of Systems, Berlin, DE, Springer, 2006, p. 350-364, ISBN 978-3-540-33056-1
2005Bouajjani Ahmed, Habermehl Peter, Moro Pierre, Vojnar Tomáš: Verifying Programs with Dynamic 1-Selector-Linked Structures in Regular Model Checking, In: Tools and Algorithms for the Construction and Analysis of Systems, Berlin, DE, Springer, 2005, p. 13-29, ISBN 978-3-540-25333-4
 Bouajjani Ahmed, Habermehl Peter, Rogalewicz Adam, Vojnar Tomáš: Abstract Regular Tree Model Checking, In: Proceedings of 7th International Workshop on Verification of Infinite-State Systems -- INFINITY 2005, Aarhus, DK, BRICS, 2005, p. 15-24, ISSN 0909-3206
 Češka Milan, Erlebach Pavel, Vojnar Tomáš: Pattern-Based Verification of Programs with Extended Linear Linked Data Structures, In: Proceedings of Fifth International Workshop on Automated Verification of Critical Systems, Warwick, GB, 2005, p. 101-117
 Češka Milan, Křena Bohuslav, Vojnar Tomáš: Parallel State Space Generation and Exploration on Shared-Memory Architectures, In: Computer Aided Systems Theory - EUROCAST 2005, Berlin, DE, Springer, 2005, p. 275-280, ISBN 978-3-540-29002-5
 Erlebach Pavel, Vojnar Tomáš: Automated Formal Verification of Programs with Dynamic Data Structures Using State-of-the-Art Tools, In: Proceedings of 8th International Conference ISIM'05 Information System Implementation and Modeling, Ostrava, CZ, MARQ, 2005, p. 219-226, ISBN 80-86840-09-3
 Erlebach Pavel: Experience from Verifying in TVLA, In: EEICT'05, Brno, CZ, FEKT VUT, 2005, p. 648-652, ISBN 80-214-2890-2
 Erlebach Pavel: Towards a Systematic Framework for Automatic Pattern-Based Verification of Dynamic Data Structures, In: PRE-PROCEEDINGS of the 1st Doctoral Workshop on Mathematical and Engineering Methods in Computer Science, Brno, CZ, FI MUNI, 2005, p. 145-154
 Habermehl Peter, Iosif Radu, Vojnar Tomáš: Automata-based Verification of Programs with Tree Updates, Verimag Technical Report number TR-2005-16, Grenoble, FR, VERIMAG, 2005, p. 28
 Habermehl Peter, Vojnar Tomáš: Regular Model Checking Using Inference of Regular Languages, In: ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, Vol. 138, No. 3, 2005, US, p. 21-36, ISSN 1571-0661
 Rogalewicz Adam: Towards Applying Mona in Abstract Regular Tree Model Checking, In: Proceedings of the 11th Conference Student EEICT 2005, Brno, CZ, FIT VUT, 2005, p. 663-667, ISBN 80-214-2890-2
2004Bouajjani Ahmed, Habermehl Peter, Vojnar Tomáš: Abstract Regular Model Checking, In: Lecture Notes in Computer Science, Vol. 2004, No. 3114, DE, p. 372-386, ISSN 0302-9743
 Habermehl Peter, Vojnar Tomáš: Regular Model Checking Using Inference of Regular Languages, In: Proceedings of 6th International Workshop on Verification of Infinite-State Systems -- INFINITY 2004, London, GB, 2004, p. 61-71
 Rogalewicz Adam, Vojnar Tomáš: Tree Automata In Modelling And Verification Of Concurrent Programs, In: Proceedings of ASIS 2004, Ostrava, CZ, MARQ, 2004, p. 197-202, ISBN 80-86840-03-4
2003Bouajjani Ahmed, Habermehl Peter, Vojnar Tomáš: Verification of Parametric Concurrent Systems with Prioritized FIFO Resource Management, In: Lecture Notes in Computer Science, Vol. 2003, No. 2761, DE, p. 174-190, ISSN 0302-9743

Your IPv4 address: 72.44.48.122
Switch to IPv6 connection

DNSSEC [dnssec]