Automatic Formal Analysis and Verification of Programs with Complex Unbounded Data and Control Structures

Reseach leader:Vojnar Tomáš
Team leaders:Kofroň Jan (MFF UK)
Team members:Dudka Kamil, Fiedor Jan, Holík Lukáš, Hruška Martin (FIT VUT), Chaloupka Jan, Lengál Ondřej, Müller Petr, Parízek Pavel (MFF UK), Peringer Petr, Rogalewicz Adam
Agency:Czech Science Foundation
Code:GA14-11384S
Start:2014-01-01
End:2016-12-31
Keywords:formal verification, symbolic verification, infinite-state systems, theory of automata, logic, dynamic linked data structures, collections, parametric systems, concurrency
Annotation:
The project targets formal verification of infinite-state software systems. In particular, it aims at improving the degree of automation, scalability, and generality of the current approaches to formal verification of programs handling unbounded data structures, such as collections or dynamic linked data structures based on pointers, possibly storing data from unbounded domains, and/or using unbounded or parametric concurrency. As for concurrent programs, the stress will be on programs using modern synchronization means such as lockless data structures or transactional memories. To handle such programs, the project focuses on extending the current and developing new symbolic verification approaches based on automata and/or logics. When working on the project, members of the project teams will build on their deep and mutually complementary expertise with abstract regular model checking, tree and forest automata, separation logic and symbolic memory graphs, predicate abstraction over primitive data and collections, and thread modular verification of concurrent programs.

Products

2015dWiNA - An Implementation of Decision Procedure for WS1S, software, 2015
Authors: Fiedor Tomáš, Lengál Ondřej, Holík Lukáš, Vojnar Tomáš
 INCLUDER (tracer): Trace Inclusion for Data Word Automata, software, 2015
Authors: Rogalewicz Adam, Iosif Radu, Vojnar Tomáš
2014HADES (Hazard Detection System), software, 2014
Authors: Charvát Lukáš, Smrčka Aleš, Vojnar Tomáš
 SLIDE: Separation Logic with Inductive Definitions, software, 2014
Authors: Rogalewicz Adam, Iosif Radu, Vojnar Tomáš
 SPEN - A Solver for Separation Logic Entailments, software, 2014
Authors: Enea Constantin, Lengál Ondřej, Sighireanu Mihaela, Vojnar Tomáš

Publications

2017ENEA Constantin, LENGÁL Ondřej, SIGHIREANU Mihaela and VOJNAR Tomáš. Compositional Entailment Checking for a Fragment of Separation Logic. Formal Methods in System Design. Berlin: Springer Verlag, 2017, vol. 2017, no. 51, pp. 575-607. ISSN 0925-9856.
 HOLÍK Lukáš, HRUŠKA Martin, LENGÁL Ondřej, ROGALEWICZ Adam and VOJNAR Tomáš. Counterexample Validation and Interpolation-Based Refinement for Forest Automata. In: Proceedings of VMCAI'17. Cham: Springer Verlag, 2017, pp. 288-309. ISBN 978-3-319-52234-0.
2016DUDKA Kamil, HOLÍK Lukáš, PERINGER Petr, TRTÍK Marek and VOJNAR Tomáš. From Low-Level Pointers to High-Level Containers. In: Verification, Model Checking, and Abstract Interpretation (VMCAI). Berlin Heidelberg: Springer Verlag, 2016, pp. 431-452. ISBN 978-3-662-49121-8.
 DUDKA Kamil, HOLÍK Lukáš, PERINGER Petr, TRTÍK Marek and VOJNAR Tomáš. From Low-Level Pointers to High-Level Containers, Technical Report No. FIT-TR-2015-03. Brno, 2016.
 HOLÍK Lukáš, HRUŠKA Martin, LENGÁL Ondřej, ROGALEWICZ Adam, ŠIMÁČEK Jiří and VOJNAR Tomáš. Run Forester, Run Backwards! (Competition Contribution). In: Proceedings of TACAS'16. Heidelberg: Springer Verlag, 2016, pp. 923-926. ISBN 978-3-662-49673-2.
 HOLÍK Lukáš, KOTOUN Michal, PERINGER Petr, ŠOKOVÁ Veronika, TRTÍK Marek and VOJNAR Tomáš. Predator Shape Analysis Tool Suite. In: Proceedings of HVC 2016. Zurich: Springer Verlag, 2016, pp. 202-209. ISBN 978-3-319-49052-6.
 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.
 CHARVÁT Lukáš, SMRČKA Aleš and VOJNAR Tomáš. Hades: Microprocessor Hazard Analysis via Formal Verification of Parameterized Systems. In: Proceedings 11th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2016). Brno: Faculty of Information Technology BUT, 2016, pp. 87-93. ISSN 2075-2180.
 IOSIF Radu, ROGALEWICZ Adam and VOJNAR Tomáš. Abstraction Refinement and Antichains for Trace Inclusion of Infinite State Systems. In: Tools and Algorithms for the Construction and Analysis of Systems. Heidelberg: Springer Verlag, 2016, pp. 71-89. ISBN 978-3-662-49673-2.
 KOTOUN Michal, PERINGER Petr, ŠOKOVÁ Veronika and VOJNAR Tomáš. Optimized PredatorHP and the SV-COMP Heap and Memory Safety Benchmark (Competition Contribution). In: Proceedings of TACAS 2016. Heidelberg: Springer Verlag, 2016, pp. 942-945. ISBN 978-3-662-49673-2.
2015ABDULLA 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.
 CHARVÁT Lukáš, SMRČKA Aleš and VOJNAR Tomáš. Microprocessor Hazard Analysis via Formal Verification of Parameterized Systems. In: Proceedings of the 15th International Conference on Computer Aided Systems Theory (EUROCAST 2015). Las Palmas de Grand Canaria: The Universidad de Las Palmas de Gran Canaria, 2015, pp. 193-194. ISBN 978-84-606-5438-4.
 MÜLLER Petr, PERINGER Petr and VOJNAR Tomáš. Predator Hunting Party (Competition Contribution). In: Proceedings of TACAS'15. Heidelberg: Springer Verlag, 2015, pp. 443-446. ISBN 978-3-662-46680-3.
2014ABDULLA 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.
 DUDKA Kamil, PERINGER Petr and VOJNAR Tomáš. Predator: A Shape Analyzer Based on Symbolic Memory Graphs (Competition Contribution). In: Tools and Algorithms for the Construction and Analysis of Systems. Heidelberg: Springer Verlag, 2014, pp. 412-414. ISBN 978-3-642-54861-1.
 ENEA Constantin, LENGÁL Ondřej, SIGHIREANU Mihaela and VOJNAR Tomáš. Compositional Entailment Checking for a Fragment of Separation Logic. In: Proceedings of APLAS'14. Heidelberg: Springer Verlag, 2014, pp. 314-333. ISBN 978-3-319-12735-4.
 ENEA Constantin, LENGÁL Ondřej, SIGHIREANU Mihaela and VOJNAR Tomáš. Compositional Entailment Checking for a Fragment of Separation Logic. FIT-TR-2014-01, Brno: Faculty of Information Technology BUT, 2014.
 FIEDOR Tomáš. A Decision Procedure For The WSkS Logic. Saarbrücken: Lambert Academic Publishing, 2014. ISBN 978-3-659-63583-0.
 CHARVÁT Lukáš, SMRČKA Aleš and VOJNAR Tomáš. Using Formal Verification of Parameterized Systems in RAW Hazard Analysis in Microprocessors. In: Proceedings of 15th International Workshop on Microprocessor Test and Verification (MTV 2014). Austin, TX: IEEE Computer Society, 2014, pp. 83-89. ISBN 978-1-4673-6858-2.
 IOSIF Radu, ROGALEWICZ Adam and VOJNAR Tomáš. Deciding Entailments in Inductive Separation Logic with Tree Automata. In: Proceedings of ATVA'14. Heidelberg: Springer Verlag, 2014, pp. 201-218. ISBN 978-3-319-11935-9.
 MÜLLER Petr and VOJNAR Tomáš. CPAlien: Shape Analyzer for CPAChecker. In: Tools and Algorithms for the Construction and Analysis of Systems. Heidelberg: Springer Verlag, 2014, pp. 395-397. ISBN 978-3-642-54861-1.

Your IPv4 address: 54.163.209.109
Switch to IPv6 connection

DNSSEC [dnssec]