Automatizovaná formální analýza a verifikace programů se složitými datovými a řídicími strukturami s předem neomezenou velikostí

Název v angličtině:Automatic Formal Analysis and Verification of Programs with Complex Unbounded Data and Control Structures
Hlavní řešitel:Vojnar Tomáš
Spoluřešitelé:Kofroň Jan (MFF UK)
Další řešitelé: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
Agentura:Grantová agentura České republiky - Standardní projekty
Kód:GA14-11384S
Zahájení:2014-01-01
Ukončení:2016-12-31
Klíčová slova: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
Anotace:
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ů.

Produkty

2015dWiNA - Implementace rozhodovací procedury pro WS1S, software, 2015
Autoři: Fiedor Tomáš, Lengál Ondřej, Holík Lukáš, Vojnar Tomáš
 INCLUDER (tracer): Nástroj pro rozhodování běhové inkluze pro automaty nad daty, software, 2015
Autoři: Rogalewicz Adam, Iosif Radu, Vojnar Tomáš
2014HADES (Hazard Detection System), software, 2014
Autoři: Charvát Lukáš, Smrčka Aleš, Vojnar Tomáš
 SLIDE: Separační logika s induktivními definicemi, software, 2014
Autoři: Rogalewicz Adam, Iosif Radu, Vojnar Tomáš
 SPEN - Rozhodovací procedura pro separační logiku, software, 2014
Autoři: Enea Constantin, Lengál Ondřej, Sighireanu Mihaela, Vojnar Tomáš

Publikace

2017ENEA Constantin, LENGÁL Ondřej, SIGHIREANU Mihaela a VOJNAR Tomáš. Compositional Entailment Checking for a Fragment of Separation Logic. Formal Methods in System Design. Berlin: Springer Verlag, 2017, roč. 2017, č. 1, s. 1-33. ISSN 0925-9856.
 HOLÍK Lukáš, HRUŠKA Martin, LENGÁL Ondřej, ROGALEWICZ Adam a VOJNAR Tomáš. Counterexample Validation and Interpolation-Based Refinement for Forest Automata. In: Proceedings of VMCAI'17. Cham: Springer Verlag, 2017, s. 288-309. ISBN 978-3-319-52234-0.
2016DUDKA Kamil, HOLÍK Lukáš, PERINGER Petr, TRTÍK Marek a VOJNAR Tomáš. From Low-Level Pointers to High-Level Containers. In: Verification, Model Checking, and Abstract Interpretation (VMCAI). Berlin Heidelberg: Springer Verlag, 2016, s. 431-452. ISBN 978-3-662-49121-8.
 DUDKA Kamil, HOLÍK Lukáš, PERINGER Petr, TRTÍK Marek a 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ří a VOJNAR Tomáš. Run Forester, Run Backwards! (Competition Contribution). In: Proceedings of TACAS'16. Heidelberg: Springer Verlag, 2016, s. 923-926. ISBN 978-3-662-49673-2.
 HOLÍK Lukáš, KOTOUN Michal, PERINGER Petr, ŠOKOVÁ Veronika, TRTÍK Marek a VOJNAR Tomáš. Predator Shape Analysis Tool Suite. In: Proceedings of HVC 2016. Zurich: Springer Verlag, 2016, s. 202-209. ISBN 978-3-319-49052-6.
 HOLÍK Lukáš, MEYER Roland a MUSKALLA Sebastian. Antichains for the Verification of Recursive Programs. In: Proceedings of International Conference on Networked Systems. Cham: Springer International Publishing, 2016, s. 322-336. ISBN 978-3-319-26849-1.
 CHARVÁT Lukáš, SMRČKA Aleš a 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: Fakulta informačních technologií VUT v Brně, 2016, s. 87-93. ISSN 2075-2180.
 IOSIF Radu, ROGALEWICZ Adam a 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, s. 71-89. ISBN 978-3-662-49673-2.
 KOTOUN Michal, PERINGER Petr, ŠOKOVÁ Veronika a VOJNAR Tomáš. Optimized PredatorHP and the SV-COMP Heap and Memory Safety Benchmark (Competition Contribution). In: Proceedings of TACAS 2016. Heidelberg: Springer Verlag, 2016, s. 942-945. ISBN 978-3-662-49673-2.
2015ABDULLA Parosh A., HOLÍK Lukáš, JONSSON Bengt, LENGÁL Ondřej, TRINH Quy Cong a VOJNAR Tomáš. Verification of heap manipulating programs with ordered data by extended forest automata. Acta Informatica. 2015, roč. 53, č. 4, s. 357-385. ISSN 0001-5903.
 FIEDOR Tomáš, HOLÍK Lukáš, LENGÁL Ondřej a VOJNAR Tomáš. Nested Antichains for WS1S. In: Proceedings of TACAS'15. Heidelberg: Springer Verlag, 2015, s. 658-674. ISBN 978-3-662-46680-3.
 HOLÍK Lukáš, HRUŠKA Martin, LENGÁL Ondřej, ROGALEWICZ Adam, ŠIMÁČEK Jiří a VOJNAR Tomáš. Forester: Shape Analysis Using Tree Automata (Competition Contribution). In: Proceedings of TACAS'15. Heidelberg: Springer Verlag, 2015, s. 431-434. ISBN 978-3-662-46680-3.
 CHARVÁT Lukáš, SMRČKA Aleš a 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: Universidad de Las Palmas de Gran Canaria, 2015, s. 193-194. ISBN 978-84-606-5438-4.
 MÜLLER Petr, PERINGER Petr a VOJNAR Tomáš. Predator Hunting Party (Competition Contribution). In: Proceedings of TACAS'15. Heidelberg: Springer Verlag, 2015, s. 443-446. ISBN 978-3-662-46680-3.
2014ABDULLA Parosh A., HAZIZA Frédéric a HOLÍK Lukáš. Block Me If You Can! Context-Sensitive Parameterized Verification. In: 21st International Static Analysis Symposium. Berlin: Springer Verlag, 2014, s. 1-17. ISBN 978-3-319-10935-0. ISSN 0302-9743.
 ABDULLA Parosh A., HOLÍK Lukáš, CHEN Yu-Fang a VOJNAR Tomáš. Mediating for reduction (on minimizing alternating Buchi automata). Theoretical Computer Science. Paris: Elsevier Science, 2014, roč. 2014, č. 552, s. 26-43. ISSN 0304-3975.
 DUDKA Kamil, PERINGER Petr a 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, s. 412-414. ISBN 978-3-642-54861-1.
 ENEA Constantin, LENGÁL Ondřej, SIGHIREANU Mihaela a VOJNAR Tomáš. Compositional Entailment Checking for a Fragment of Separation Logic. In: Proceedings of APLAS'14. Heidelberg: Springer Verlag, 2014, s. 314-333. ISBN 978-3-319-12735-4.
 ENEA Constantin, LENGÁL Ondřej, SIGHIREANU Mihaela a VOJNAR Tomáš. Compositional Entailment Checking for a Fragment of Separation Logic. FIT-TR-2014-01, Brno: Fakulta informačních technologií VUT v Brně, 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š a 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, s. 83-89. ISBN 978-1-4673-6858-2.
 IOSIF Radu, ROGALEWICZ Adam a VOJNAR Tomáš. Deciding Entailments in Inductive Separation Logic with Tree Automata. In: Proceedings of ATVA'14. Heidelberg: Springer Verlag, 2014, s. 201-218. ISBN 978-3-319-11935-9.
 MÜLLER Petr a VOJNAR Tomáš. CPAlien: Shape Analyzer for CPAChecker (Competition Contribution). In: Tools and Algorithms for the Construction and Analysis of Systems. Heidelberg: Springer Verlag, 2014, s. 395-397. ISBN 978-3-642-54861-1.

Vaše IPv4 adresa: 54.221.73.186
Přepnout na IPv6 spojení

DNSSEC [dnssec]