Project Details
Rozvoj technik pro automatické verifikace programů s dynamickými datovými strukturami
Project Period: 1. 1. 2009 – 31. 12. 2011
Project Type: grant
Code: GP201/09/P531
Agency: Czech Science Foundation
Program: Standardní projekty
formal verification, model checking, infinite state-space systems, dynamic data structures
Use of the dynamic data structures is a common technique used in all bigger software systems. On the other hand, searching for errors in such systems is very complicated thanks to the fact that the data structure itself is hidden behind the tricky pointer manipulations. Hence the automated methods for such programs are greatly welcome. The whole verification problem is much more complicated in the case, where several concurrent processes use a shared memory. Bad interference of one of these processes into a dynamic data structure inside the shared memory can interferes the other processes. Another complication for the verification is recursive functions calls. Despite of the huge progress in this area, a reliable verification tool for common use is still far away. Therefore the goal of the proposed basic research project is development of methods for this class of programs.
2012
- HOLÍK, L.; ROGALEWICZ, A.; ŠIMÁČEK, J.; VOJNAR, T.; HABERMEHL, P. Forest Automata for Verification of Heap Manipulation. FORMAL METHODS IN SYSTEM DESIGN, 2012, vol. 2012, no. 41,
p. 83-106. ISSN: 0925-9856. Detail - ROGALEWICZ, A.; VOJNAR, T.; HABERMEHL, P.; BOUAJJANI, A. Abstract Regular (Tree) Model Checking. International Journal on Software Tools for Technology Transfer, 2012, vol. 14, no. 2,
p. 167-191. ISSN: 1433-2779. Detail
2011
- HOLÍK, L.; ROGALEWICZ, A.; ŠIMÁČEK, J.; VOJNAR, T.; HABERMEHL, P. Forest Automata for Verification of Heap Manipulation. Lecture Notes in Computer Science, 2011, vol. 2011, no. 6806,
p. 424-440. ISSN: 0302-9743. Detail
2010
- HOLÍK, L.; ŠIMÁČEK, J. Optimizing an LTS-Simulation Algorithm. Computing and Informatics, 2010, vol. 2010, no. 7,
p. 1337-1348. ISSN: 1335-9150. Detail
2009
- HOLÍK, L.; ŠIMÁČEK, J. Optimizing an LTS-Simulation Algorithm. 5th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science. Znojmo: Faculty of Informatics MU, 2009.
p. 93-101. ISBN: 978-3-939897-15-6. Detail - IOSIF, R.; ROGALEWICZ, A. Automata-Based Termination Proofs. Implementation and Application of Automata. Lecture Notes in Computer Science. Berlin: Springer Verlag, 2009.
p. 165-177. ISBN: 978-3-642-02978-3. Detail