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 verification
infinite state systems
pointer programs
string manipulating programs
symbolic encoding
regular model checking
finite automata
language inclusion
minimization
simulation 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. (UITS FIT VUT) , research leader
Lengál Ondřej, Ing., Ph.D. (UITS FIT VUT)
Publications

2017

  • ABDULLA Parosh A., HAZIZA Frédéric, HOLÍK Lukáš, JONSSON Bengt and REZINE Ahmed. An integrated specification and verification technique for highly concurrent data structures for highly concurrent data structures. International Journal on Software Tools for Technology Transfer, vol. 5, no. 19, 2017, pp. 549-563. ISSN 1433-2779. Detail

2016

  • HOLÍK Lukáš, MEYER Roland and MUSKALLA Sebastian. 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, pp. 322-336. ISBN 978-3-319-26849-1. Detail
  • HAZIZA Frédéric, HOLÍK Lukáš, MEYER Roland and WOLF Sebastian. Pointer Race Freedom. In: Verification, Model Checking, and Abstract Interpretation (VMCAI). Lecture Notes in Computer Science, vol. 9583. Berlin: Springer Verlag, 2016, pp. 393-412. ISBN 978-3-662-49121-8. Detail

2015

  • HOLÍK Lukáš, HRUŠKA Martin, LENGÁL Ondřej, ROGALEWICZ Adam, ŠIMÁČEK Jiří and VOJNAR Tomáš. Forester: Shape Analysis Using Tree Automata (Competition Contribution). In: Proceedings of TACAS'15. Lecture Notes in Computer Science, vol. 9035. Heidelberg: Springer Verlag, 2015, pp. 432-435. ISBN 978-3-662-46680-3. Detail
  • HOLÍK Lukáš, ISBERNER Malte and JONSSON Bengt. Mediator Synthesis in a Component Algebra with Data. In: Correct System Design. Lecture Notes in Computer Science. Berlin: Springer Verlag, 2015, pp. 238-259. ISBN 978-3-319-23505-9. Detail
  • FIEDOR Tomáš, HOLÍK Lukáš, LENGÁL Ondřej and VOJNAR Tomáš. Nested Antichains for WS1S. In: Proceedings of TACAS'15. Lecture Notes in Computer Science, vol. 9035. Heidelberg: Springer Verlag, 2015, pp. 658-674. ISBN 978-3-662-46680-3. Detail
  • ABDULLA Parosh A., ATIG Mohamed F., HOLÍK Lukáš, CHEN Yu-Fang, REZINE Ahmed, RUMMER Philipp and STENMAN Jari. Norn: An SMT Solver for String Constraints. In: Computer Aided Verification. Lecture Notes in Computer Science Volume 9206. Cham: Springer International Publishing, 2015, pp. 462-469. ISBN 978-3-319-21689-8. Detail
  • ABDULLA Parosh A., HAZIZA Frédéric and HOLÍK Lukáš. Parameterized verification through view abstraction. International Journal on Software Tools for Technology Transfer, vol. 2016, no. 5, 2015, pp. 495-516. ISSN 1433-2779. Detail
  • ABDULLA Parosh A., HOLÍK Lukáš, JONSSON Bengt, LENGÁL Ondřej, TRINH Quy Cong and VOJNAR Tomáš. Verification of heap manipulating programs with ordered data by extended forest automata. Acta Informatica, vol. 53, no. 4, 2015, pp. 357-385. ISSN 0001-5903. Detail
  • ABDULLA Parosh A., HAZIZA Frédéric and HOLÍK Lukáš. View Abstraction - A Tutorial. In: 2nd International Workshop on Synthesis of Complex Parameters. OpenAccess Series in Informatics, vol. 44. Dagstuhl: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2015, pp. 1-15. ISBN 978-3-939897-82-8. ISSN 2190-6807. Detail

2014

  • ABDULLA Parosh A., HAZIZA Frédéric and HOLÍK Lukáš. Block Me If You Can! Context-Sensitive Parameterized Verification. In: 21st International Static Analysis Symposium. Lecture Notes in Computer Science, vol. 2014. Berlin: Springer Verlag, 2014, pp. 1-17. ISBN 978-3-319-10935-0. ISSN 0302-9743. Detail
  • ABDULLA Parosh A., HOLÍK Lukáš, CHEN Yu-Fang and VOJNAR Tomáš. Mediating for reduction (on minimizing alternating Buchi automata). Theoretical Computer Science, vol. 2014, no. 552, pp. 26-43. ISSN 0304-3975. Detail
  • ABDULLA Parosh A., ATIG Mohamed F., HOLÍK Lukáš, CHEN Yu-Fang, RUMMER Philipp and STENMAN Jari. String Constraints for Verification. In: 26th International Conference on Computer Aided Verification. Lecture Notes in Computer Science, Volume 8559, vol. 8559. Berlin: Springer Verlag, 2014, pp. 150-166. ISBN 978-3-319-08866-2. Detail

2013

  • HOLÍK Lukáš, LENGÁL Ondřej, ROGALEWICZ Adam, ŠIMÁČEK Jiří and VOJNAR Tomáš. Fully Automated Shape Analysis Based on Forest Automata. In: Proceedings of CAV'13. Heidelberg: Springer Verlag, 2013, pp. 740-755. ISBN 978-3-642-39798-1. ISSN 0302-9743. Detail
  • HOLÍK Lukáš, LENGÁL Ondřej, ROGALEWICZ Adam, ŠIMÁČEK Jiří and VOJNAR Tomáš. Fully Automated Shape Analysis Based on Forest Automata. FIT-TR-2013-01, Brno: Faculty of Information Technology BUT, 2013. Detail
  • ABDULLA Parosh A., HOLÍK Lukáš, JONSSON Bengt, LENGÁL Ondřej, TRINH Quy Cong and VOJNAR Tomáš. Verification of Heap Manipulating Programs with Ordered Data by Extended Forest Automata. In: Proceedings of ATVA'13. Heidelberg: Springer Verlag, 2013, pp. 224-239. ISBN 978-3-319-02443-1. Detail
  • ABDULLA Parosh A., HOLÍK Lukáš, JONSSON Bengt, LENGÁL Ondřej, TRINH Quy Cong and VOJNAR Tomáš. Verification of Heap Manipulating Programs with Ordered Data by Extended Forest Automata. FIT-TR-2013-02, Brno: Faculty of Information Technology BUT, 2013. Detail
Products

2015

  • dWiNA - An Implementation of Decision Procedure for WS1S, software, 2015
    Authors: Fiedor Tomáš, Lengál Ondřej, Holík Lukáš, Vojnar Tomáš Detail
Back to top