Project Details
Verification of Infinite State Systems Based on Finite Automata
Project Period: 1. 2. 2013 – 31. 12. 2015
Project Type: grant
Code: GP13-37876P
Agency: Czech Science Foundation
Program: Postdoktorandské granty
formal verificationinfinite state systemspointer programsstring manipulating
programssymbolic encodingregular model checkingfinite automatalanguage
inclusionminimizationsimulation relation
The focus of this project is formal verification of programs with infinite state
spaces. Specifically, we target programs with dynamically allocated pointer data
structures and programs manipulating unbounded strings. Verification methods for
both of these classes are highly desirable. The former are notoriously
error-prone, hard to debug and reason about, and the latter form the main body of
web applications where errors may easily lead to security vulnerabilities. We
will build on methods based on symbolically encoding sets of program states using
finite automata, such as regular model checking. In a connection to that, we will
also investigate theory and methods facilitating practical use of finite automata
in general. This especially concerns language inclusion and equivalence testing,
size reduction and minimization, and decision procedures for the logics WSkS and
MSO. The work on the project will include rigorous mathematical description of
the developed principles and algorithms as well as their implementation and
experimental evaluation.
2017
- HOLÍK, L.; ABDULLA, P.; HAZIZA, F.; JONSSON, B.; REZINE, A. An integrated specification and verification technique for highly concurrent data structures for highly concurrent data structures. International Journal on Software Tools for Technology Transfer, 2017, vol. 5, no. 19,
p. 549-563. ISSN: 1433-2779. Detail
2016
- HOLÍK, L.; MEYER, R.; MUSKALLA, S. Antichains for the Verification of Recursive Programs. In Proceedings of International Conference on Networked Systems. Lecture Notes in Computer Science (LNCS). Cham: Springer International Publishing, 2016.
p. 322-336. ISBN: 978-3-319-26849-1. Detail - HOLÍK, L.; MEYER, R.; WOLF, S.; HAZIZA, F. Pointer Race Freedom. In Verification, Model Checking, and Abstract Interpretation (VMCAI). Lecture Notes in Computer Science. Berlin: Springer Verlag, 2016.
p. 393-412. ISBN: 978-3-662-49121-8. Detail
2015
- FIEDOR, T.; HOLÍK, L.; LENGÁL, O.; VOJNAR, T. Nested Antichains for WS1S. In Proceedings of TACAS'15. Lecture Notes in Computer Science. Heidelberg: Springer Verlag, 2015.
p. 658-674. ISBN: 978-3-662-46680-3. Detail - HOLÍK, L.; ABDULLA, P.; HAZIZA, F. Parameterized verification through view abstraction. International Journal on Software Tools for Technology Transfer, 2015, vol. 2016, no. 5,
p. 495-516. ISSN: 1433-2779. Detail - HOLÍK, L.; CHEN, Y.; REZINE, A.; RUMMER, P.; STENMAN, J.; ABDULLA, P.; ATIG, M. Norn: An SMT Solver for String Constraints. In Computer Aided Verification. Lecture Notes in Computer Science Volume 9206. Cham: Springer International Publishing, 2015.
p. 462-469. ISBN: 978-3-319-21689-8. Detail - HOLÍK, L.; HAZIZA, F.; ABDULLA, P. View Abstraction - A Tutorial. In 2nd International Workshop on Synthesis of Complex Parameters. OpenAccess Series in Informatics (OASIcs). OpenAccess Series in Informatics. Dagstuhl: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2015.
p. 1-15. ISBN: 978-3-939897-82-8. ISSN: 2190-6807. Detail - HOLÍK, L.; ISBERNER, M.; JONSSON, B. Mediator Synthesis in a Component Algebra with Data. In Correct System Design. Lecture Notes in Computer Science. Berlin: Springer Verlag, 2015.
p. 238-259. ISBN: 978-3-319-23505-9. Detail - HOLÍK, L.; LENGÁL, O.; VOJNAR, T.; JONSSON, B.; TRINH, Q.; ABDULLA, P. Verification of heap manipulating programs with ordered data by extended forest automata. Acta Informatica, 2015, vol. 53, no. 4,
p. 357-385. ISSN: 0001-5903. Detail - HRUŠKA, M.; LENGÁL, O.; ŠIMÁČEK, J.; VOJNAR, T.; HOLÍK, L.; ROGALEWICZ, A. Forester: Shape Analysis Using Tree Automata (Competition Contribution). In Proceedings of TACAS'15. Lecture Notes in Computer Science. Heidelberg: Springer Verlag, 2015.
p. 432-435. ISBN: 978-3-662-46680-3. Detail
2014
- ABDULLA, P.; HAZIZA, F.; HOLÍK, L. Block Me If You Can! Context-Sensitive Parameterized Verification. In 21st International Static Analysis Symposium. Lecture Notes in Computer Science. Lecture Notes in Computer Science. Berlin: Springer Verlag, 2014.
p. 1-17. ISBN: 978-3-319-10935-0. ISSN: 0302-9743. Detail - HOLÍK, L.; ABDULLA, P.; ATIG, M.; CHEN, Y.; RUMMER, P.; STENMAN, J. String Constraints for Verification. In 26th International Conference on Computer Aided Verification. Lecture Notes in Computer Science, Volume 8559. Berlin: Springer Verlag, 2014.
p. 150-166. ISBN: 978-3-319-08866-2. Detail - HOLÍK, L.; VOJNAR, T.; ABDULLA, P.; CHEN, Y. Mediating for reduction (on minimizing alternating Buchi automata). Theoretical Computer Science, 2014, vol. 2014, no. 552,
p. 26-43. ISSN: 0304-3975. Detail
2013
- HOLÍK, L.; JONSSON, B.; LENGÁL, O.; VOJNAR, T.; TRINH, Q.; ABDULLA, P. Verification of Heap Manipulating Programs with Ordered Data by Extended Forest Automata. FIT-TR-2013-02, Brno: Faculty of Information Technology BUT, 2013.
p. 1-35. Detail - HOLÍK, L.; JONSSON, B.; LENGÁL, O.; VOJNAR, T.; TRINH, Q.; ABDULLA, P. Verification of Heap Manipulating Programs with Ordered Data by Extended Forest Automata. Proceedings of ATVA'13. Heidelberg: Springer Verlag, 2013.
p. 224-239. ISBN: 978-3-319-02443-1. Detail - HOLÍK, L.; LENGÁL, O.; ROGALEWICZ, A.; ŠIMÁČEK, J.; VOJNAR, T. Fully Automated Shape Analysis Based on Forest Automata. FIT-TR-2013-01, Brno: Faculty of Information Technology BUT, 2013.
p. 1-25. Detail - HOLÍK, L.; LENGÁL, O.; ROGALEWICZ, A.; ŠIMÁČEK, J.; VOJNAR, T. Fully Automated Shape Analysis Based on Forest Automata. Proceedings of CAV'13. Lecture Notes in Computer Science. Heidelberg: Springer Verlag, 2013.
p. 740-755. ISBN: 978-3-642-39798-1. ISSN: 0302-9743. Detail