Department of Intelligent Systems

Verification of Infinite State Systems Based on Finite Automata

Czech title:Verifikace nekonečně stavových systémů založená na konečných automatech
Reseach leader:Holík Lukáš
Team members:Lengál Ondřej
Agency:Czech Science Foundation
Code:GP13-37876P
Start:2013-02-01
End:2015-12-31
Keywords:
formal verification
infinite state systems
pointer programs
string manipulating programs
symbolic encoding
regular model checking
finite automata
language inclusion
minimization
simulation relation
Annotation:
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.

Products

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

Publications

2016HAZIZA Frédéric, HOLÍK Lukáš, MEYER Roland and WOLF Sebastian. Pointer Race Freedom. In: Verification, Model Checking, and Abstract Interpretation (VMCAI). Berlin: Springer Verlag, 2016, pp. 393-412. ISBN 978-3-662-49121-8.
 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. Cham: Springer International Publishing, 2016, pp. 322-336. ISBN 978-3-319-26849-1.
2015ABDULLA 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. Cham: Springer International Publishing, 2015, pp. 462-469. ISBN 978-3-319-21689-8.
 ABDULLA Parosh A., HAZIZA Frédéric and HOLÍK Lukáš. Parameterized verification through view abstraction. International Journal on Software Tools for Technology Transfer. 2015, vol. 2016, no. 5, pp. 495-516. ISSN 1433-2779.
 ABDULLA Parosh A., HAZIZA Frédéric and HOLÍK Lukáš. View Abstraction - A Tutorial. In: 2nd International Workshop on Synthesis of Complex Parameters. Dagstuhl: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2015, pp. 1-15. ISBN 978-3-939897-82-8.
 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. 2015, vol. 53, no. 4, pp. 357-385. ISSN 0001-5903.
 FIEDOR Tomáš, HOLÍK Lukáš, LENGÁL Ondřej and VOJNAR Tomáš. Nested Antichains for WS1S. In: Proceedings of TACAS'15. Heidelberg: Springer Verlag, 2015, pp. 658-674. ISBN 978-3-662-46680-3.
 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. Heidelberg: Springer Verlag, 2015, pp. 431-434. ISBN 978-3-662-46680-3.
 HOLÍK Lukáš, ISBERNER Malte and JONSSON Bengt. Mediator Synthesis in a Component Algebra with Data. In: Correct System Design. Berlin: Springer Verlag, 2015, pp. 238-259. ISBN 978-3-319-23505-9.
2014ABDULLA 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. Berlin: Springer Verlag, 2014, pp. 150-166. ISBN 978-3-319-08866-2.
 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. Berlin: Springer Verlag, 2014, pp. 1-17. ISBN 978-3-319-10935-0. ISSN 0302-9743.
 ABDULLA Parosh A., HOLÍK Lukáš, CHEN Yu-Fang and VOJNAR Tomáš. Mediating for reduction (on minimizing alternating Buchi automata). Theoretical Computer Science. Paris: Elsevier Science, 2014, vol. 2014, no. 552, pp. 26-43. ISSN 0304-3975.
2013ABDULLA 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.
 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.
 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.
 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.

Your IPv4 address: 54.224.50.28
Switch to IPv6 connection

DNSSEC [dnssec]