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

Czech title
Verifikace nekonečně stavových systémů založená na konečných automatech
Type
grant
Keywords

formal verificationinfinite state systemspointer programsstring manipulating programssymbolic encodingregular model checkingfinite automatalanguage inclusionminimizationsimulation relation

Abstract

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.

Team members
Holík Lukáš, doc. Mgr., Ph.D. (DITS) – research leader
Lengál Ondřej, Ing., Ph.D. (DITS)
Publications

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. An Anti Chain-based Approach to Recursive Program Verification. 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. 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. 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
Back to top