Project detail

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

Duration: 01.01.2014 — 31.12.2016

Funding resources

Czech Science Foundation - Standardní projekty

- whole funder (2014-01-01 - 2016-12-31)

On the project

Projekt směřuje do oblasti formální verifikace nekonečně stavových softwarových systémů. Konkrétně se soustředí na zvýšení automatizace, škálovatelnosti a obecnosti současných metod formální verifikace programů s neomezenými datovými strukturami, jako jsou ukazatelové struktury a kolekce, obsahujícími data z případně neomezených domén a/nebo používající neomezený či parametrický paralelismus. V případě paralelních programů bude kladen důraz zejména na programy používající moderní synchronizační prostředky, jako jsou bezzámkové struktury či transakční paměti. S cílem umožnit verifikaci takových programů se projekt zaměřuje na rozvoj stávajících a návrh nových metod symbolické verifikace založených na využití automatů a logik. Při jeho řešení budou řešitelé konkrétně vycházet ze svých hlubokých a vzájemně se doplňujících zkušeností s abstraktním regulárním model checkingem, automaty nad stromy a lesy, separační logikou a symbolickými grafy paměti, predikátovou abstrakcí pro data a kolekce a vláknově modulární verifikací paralelních programů.

Description in English
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.

Keywords
formální verifikace, symbolická verifikace, nekonečně stavové systémy, teorie automatů, logika, dynamické struktury založené na ukazatelích, kolekce, parametrické systémy, paralelismus

Key words in English
formal verification, symbolic verification, infinite-state systems, theory of automata, logic, dynamic linked data structures, collections, parametric systems, concurrency

Mark

GA14-11384S

Default language

Czech

People responsible

Dudka Kamil, Ing. - fellow researcher
Fiedor Jan, Ing., Ph.D. - fellow researcher
Holík Lukáš, doc. Mgr., Ph.D. - fellow researcher
Hruška Martin, Ing., Ph.D. - fellow researcher
Chaloupka Jan, Ing. - fellow researcher
Lengál Ondřej, Ing., Ph.D. - fellow researcher
Müller Petr, Ing. - fellow researcher
Parízek Pavel, doc. RNDr., Ph.D. - fellow researcher
Peringer Petr, Dr. Ing. - fellow researcher
Rogalewicz Adam, doc. Mgr., Ph.D. - fellow researcher
Vojnar Tomáš, prof. Ing., Ph.D. - principal person responsible

Units

Department of Intelligent Systems
- beneficiary (2013-04-10 - 2016-12-31)

Results

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

ŠIMKOVÁ, H.; KŘENA, B.; VOJNAR, T.; LETKO, Z.; UR, S.; DUDKA, V.; VOLKOVICH, Z.; AVROS, R. Boosted Decision Trees for Behaviour Mining of Concurrent Programs. Concurrency Computation Practice and Experience, 2017, vol. 29, no. 21, p. 4268-4289. ISSN: 1532-0634.
Detail

LENGÁL, O.; VOJNAR, T.; ENEA, C.; SIGHIREANU, M. Compositional Entailment Checking for a Fragment of Separation Logic. FORMAL METHODS IN SYSTEM DESIGN, 2017, vol. 2017, no. 51, p. 575-607. ISSN: 0925-9856.
Detail

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.; HRUŠKA, M.; LENGÁL, O.; ROGALEWICZ, A.; VOJNAR, T. Counterexample Validation and Interpolation-Based Refinement for Forest Automata. In Proceedings of VMCAI'17. Lecture Notes in Computer Science. Lecture Notes in Computer Science. Cham: Springer Verlag, 2017. p. 288-309. ISBN: 978-3-319-52234-0. ISSN: 0302-9743.
Detail

DUDKA, K.; PERINGER, P.; VOJNAR, T. Predator: A Shape Analyzer Based on Symbolic Memory Graphs (Competition Contribution). In Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science. Heidelberg: Springer Verlag, 2014. p. 412-414. ISBN: 978-3-642-54861-1.
Detail

MÜLLER, P.; VOJNAR, T. CPAlien: Shape Analyzer for CPAChecker. In Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science. Heidelberg: Springer Verlag, 2014. p. 395-397. ISBN: 978-3-642-54861-1.
Detail

ENEA, C.; LENGÁL, O.; SIGHIREANU, M.; VOJNAR, T. Compositional Entailment Checking for a Fragment of Separation Logic. In Proceedings of APLAS'14. Lecture Notes in Computer Science. Heidelberg: Springer Verlag, 2014. p. 314-333. ISBN: 978-3-319-12735-4.
Detail

ROGALEWICZ, A.; VOJNAR, T.; IOSIF, R. Deciding Entailments in Inductive Separation Logic with Tree Automata. In Proceedings of ATVA'14. Lecture Notes in Computer Science. Heidelberg: Springer Verlag, 2014. p. 201-218. ISBN: 978-3-319-11935-9.
Detail

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.; 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

FIEDOR, T. A Decision Procedure For The WSkS Logic. Saarbrücken: Lambert Academic Publishing, 2014. 60 p. ISBN: 978-3-659-63583-0.
Detail

CHARVÁT, L.; SMRČKA, A.; VOJNAR, T. 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. p. 83-89. ISBN: 978-1-4673-6858-2.
Detail

CHARVÁT, L.; SMRČKA, A.; VOJNAR, T. Microprocessor Hazard Analysis via Formal Verification of Parameterized Systems. 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. p. 193-194. ISBN: 978-84-606-5438-4.
Detail

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

DUDKA, K.; HOLÍK, L.; PERINGER, P.; TRTÍK, M.; VOJNAR, T. From Low-Level Pointers to High-Level Containers, Technical Report No. FIT-TR-2015-03. Brno: 2016. p. 1-28.
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

PERINGER, P.; MÜLLER, P.; VOJNAR, T. Predator Hunting Party (Competition Contribution). In Proceedings of TACAS'15. Lecture Notes in Computer Science. Heidelberg: Springer Verlag, 2015. p. 443-446. ISBN: 978-3-662-46680-3.
Detail

CHARVÁT, L.; SMRČKA, A.; VOJNAR, T. Microprocessor Hazard Analysis via Formal Verification of Parameterized Systems. In Computer Aided Systems Theory - EUROCAST 2015. Lecture Notes in Computer Science. Lecture Notes in Computer Science. Zurich: Springer International Publishing, 2015. p. 605-614. ISBN: 978-3-319-27340-2. ISSN: 0302-9743.
Detail

ROGALEWICZ, A.; VOJNAR, T.; IOSIF, R. Abstraction Refinement and Antichains for Trace Inclusion of Infinite State Systems. In Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science. Heidelberg: Springer Verlag, 2016. p. 71-89. ISBN: 978-3-662-49673-2.
Detail

DUDKA, K.; HOLÍK, L.; PERINGER, P.; TRTÍK, M.; VOJNAR, T. From Low-Level Pointers to High-Level Containers. In Verification, Model Checking, and Abstract Interpretation (VMCAI). Lecture Notes in Computer Science. Berlin Heidelberg: Springer Verlag, 2016. p. 431-452. ISBN: 978-3-662-49121-8.
Detail

HRUŠKA, M.; LENGÁL, O.; ŠIMÁČEK, J.; VOJNAR, T.; HOLÍK, L.; ROGALEWICZ, A. Run Forester, Run Backwards! (Competition Contribution). In Proceedings of TACAS'16. Lecture Notes in Computer Science. Heidelberg: Springer Verlag, 2016. p. 923-926. ISBN: 978-3-662-49673-2.
Detail

KOTOUN, M.; PERINGER, P.; ŠOKOVÁ, V.; VOJNAR, T. Optimized PredatorHP and the SV-COMP Heap and Memory Safety Benchmark (Competition Contribution). In Proceedings of TACAS 2016. Lecture Notes in Computer Science. Heidelberg: Springer Verlag, 2016. p. 942-945. ISBN: 978-3-662-49673-2.
Detail

PERINGER, P.; ŠOKOVÁ, V.; TRTÍK, M.; VOJNAR, T.; HOLÍK, L.; KOTOUN, M. Predator Shape Analysis Tool Suite. In Proceedings of HVC 2016. Lecture Notes in Computer Science. Zurich: Springer International Publishing, 2016. p. 202-209. ISBN: 978-3-319-49052-6.
Detail

CHARVÁT, L.; SMRČKA, A.; VOJNAR, T. 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). Electronic Proceedings in Theoretical Computer Science, EPTCS. Electronic Proceedings in Theoretical Computer Science. Brno: Faculty of Informatics MU, 2016. p. 87-93. ISBN: 978-80-210-8362-2. ISSN: 2075-2180.
Detail

ROGALEWICZ, A.; IOSIF, R.; VOJNAR, T.: TRACER; INCLUDER (tracer): Trace Inclusion for Data Word Automata. Nástroj i dokumentaci lze získat na URL: http://www.fit.vutbr.cz/research/groups/verifit/tools/includer/. URL: https://www.fit.vut.cz/research/product/422/. (software)
Detail

FIEDOR, T.; LENGÁL, O.; HOLÍK, L.; VOJNAR, T.: dwina; dWiNA - An Implementation of Decision Procedure for WS1S. Nástroj i dokumentaci lze získat na URL:http://www.fit.vutbr.cz/research/groups/verifit/tools/dWiNA/. URL: https://www.fit.vut.cz/research/product/432/. (software)
Detail

CHARVÁT, L.; SMRČKA, A.; VOJNAR, T.: HADES; HADES (Hazard Detection System). http://www.fit.vutbr.cz/research/groups/verifit/tools/hades/. URL: http://www.fit.vutbr.cz/research/groups/verifit/tools/hades/. (software)
Detail

LENGÁL, O.; VOJNAR, T.; ENEA, C.; SIGHIREANU, M.: spen; SPEN - A Solver for Separation Logic Entailments. http://www.liafa.univ-paris-diderot.fr/spen/. URL: http://www.liafa.univ-paris-diderot.fr/spen/. (software)
Detail

ROGALEWICZ, A.; IOSIF, R.; VOJNAR, T.: SLIDE; SLIDE: Separation Logic with Inductive Definitions. Nástroj i dokumentaci lze získat na URL: http://www.fit.vutbr.cz/research/groups/verifit/tools/slide/. URL: https://www.fit.vut.cz/research/product/373/. (software)
Detail

Responsibility: Vojnar Tomáš, prof. Ing., Ph.D.