Detail projektu

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

Období řešení: 1. 1. 2014 - 31. 12. 2016

Typ projektu: grant

Kód: GA14-11384S

Agentura: Grantová agentura České republiky

Program: Standardní projekty

Název anglicky
Automatic Formal Analysis and Verification of Programs with Complex Unbounded Data and Control Structures
Typ
grant
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

Abstrakt

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

Řešitelé
Vojnar Tomáš, prof. Ing., Ph.D. (UITS FIT VUT) , hlavní řešitel
Kofroň Jan, doc. RNDr., Ph.D. (MFF UK) , spoluřešitel
Dudka Kamil, Ing. (UITS FIT VUT)
Fiedor Jan, Ing., Ph.D. (UITS FIT VUT)
Holík Lukáš, doc. Mgr., Ph.D. (UITS FIT VUT)
Hruška Martin, Ing., Ph.D. (FIT VUT)
Chaloupka Jan, Ing. (UITS FIT VUT)
Charvát Lukáš, Ing. (UITS FIT VUT)
Lengál Ondřej, Ing., Ph.D. (UITS FIT VUT)
Müller Petr, Ing. (UITS FIT VUT)
Parízek Pavel, RNDr., Ph.D. (MFF UK)
Peringer Petr, Dr. Ing. (UITS FIT VUT)
Rogalewicz Adam, doc. Mgr., Ph.D. (UITS FIT VUT)
Publikace

2017

  • AVROS Renata, DUDKA Vendula, KŘENA Bohuslav, LETKO Zdeněk, PLUHÁČKOVÁ Hana, UR Shmuel, VOJNAR Tomáš a VOLKOVICH Zeev. Boosted decision trees for behaviour mining of concurrent programmes. Concurrency and Computation: Practice and Experience, roč. 29, č. 21, 2017, s. 4268-4289. ISSN 1532-0634. Detail
  • ENEA Constantin, LENGÁL Ondřej, SIGHIREANU Mihaela a VOJNAR Tomáš. Compositional Entailment Checking for a Fragment of Separation Logic. Formal Methods in System Design, roč. 2017, č. 51, s. 575-607. ISSN 0925-9856. Detail
  • 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. Lecture Notes in Computer Science, roč. 10145. Cham: Springer Verlag, 2017, s. 288-309. ISBN 978-3-319-52234-0. ISSN 0302-9743. Detail

2016

  • 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. Lecture Notes in Computer Science, roč. 9636. Heidelberg: Springer Verlag, 2016, s. 71-89. ISBN 978-3-662-49673-2. Detail
  • HOLÍK Lukáš, MEYER Roland a MUSKALLA Sebastian. Antichains for the Verification of Recursive Programs. In: Proceedings of International Conference on Networked Systems. Lecture Notes in Computer Science (LNCS). Cham: Springer International Publishing, 2016, s. 322-336. ISBN 978-3-319-26849-1. Detail
  • DUDKA 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). Lecture Notes in Computer Science, roč. 9583. Berlin Heidelberg: Springer Verlag, 2016, s. 431-452. ISBN 978-3-662-49121-8. Detail
  • 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. Detail
  • 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). Electronic Proceedings in Theoretical Computer Science, roč. 2016. Brno: Fakulta informatiky MU, 2016, s. 87-93. ISBN 978-80-210-8362-2. ISSN 2075-2180. Detail
  • 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. Lecture Notes in Computer Science, roč. 9636. Heidelberg: Springer Verlag, 2016, s. 942-945. ISBN 978-3-662-49673-2. Detail
  • 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. Lecture Notes in Computer Science, roč. 10028. Zurich: Springer International Publishing, 2016, s. 202-209. ISBN 978-3-319-49052-6. Detail
  • 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. Lecture Notes in Computer Science, roč. 9636. Heidelberg: Springer Verlag, 2016, s. 923-926. ISBN 978-3-662-49673-2. Detail

2015

  • 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. Lecture Notes in Computer Science, roč. 9035. Heidelberg: Springer Verlag, 2015, s. 432-435. ISBN 978-3-662-46680-3. Detail
  • 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. Detail
  • CHARVÁT Lukáš, SMRČKA Aleš a VOJNAR Tomáš. Microprocessor Hazard Analysis Via Formal Verification of Parameterized Systems. In: Computer Aided Systems Theory - EUROCAST 2015. Lecture Notes in Computer Science, roč. 9520. Zurich: Springer International Publishing, 2015, s. 605-614. ISBN 978-3-319-27340-2. ISSN 0302-9743. Detail
  • FIEDOR Tomáš, HOLÍK Lukáš, LENGÁL Ondřej a VOJNAR Tomáš. Nested Antichains for WS1S. In: Proceedings of TACAS'15. Lecture Notes in Computer Science, roč. 9035. Heidelberg: Springer Verlag, 2015, s. 658-674. ISBN 978-3-662-46680-3. Detail
  • MÜLLER Petr, PERINGER Petr a VOJNAR Tomáš. Predator Hunting Party (Competition Contribution). In: Proceedings of TACAS'15. Lecture Notes in Computer Science, roč. 9035. Heidelberg: Springer Verlag, 2015, s. 443-446. ISBN 978-3-662-46680-3. Detail
  • ABDULLA 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, roč. 53, č. 4, 2015, s. 357-385. ISSN 0001-5903. Detail

2014

  • FIEDOR Tomáš. A Decision Procedure For The WSkS Logic. Saarbrücken: Lambert Academic Publishing, 2014. ISBN 978-3-659-63583-0. Detail
  • ABDULLA 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. Lecture Notes in Computer Science, roč. 2014. Berlin: Springer Verlag, 2014, s. 1-17. ISBN 978-3-319-10935-0. ISSN 0302-9743. Detail
  • 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. Lecture Notes in Computer Science, roč. 8858. Heidelberg: Springer Verlag, 2014, s. 314-333. ISBN 978-3-319-12735-4. Detail
  • 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. Detail
  • MÜLLER Petr a VOJNAR Tomáš. CPAlien: Shape Analyzer for CPAChecker (Competition Contribution). In: Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, roč. 8413. Heidelberg: Springer Verlag, 2014, s. 395-397. ISBN 978-3-642-54861-1. Detail
  • IOSIF Radu, ROGALEWICZ Adam a VOJNAR Tomáš. Deciding Entailments in Inductive Separation Logic with Tree Automata. In: Proceedings of ATVA'14. Lecture Notes in Computer Science, roč. 8837. Heidelberg: Springer Verlag, 2014, s. 201-218. ISBN 978-3-319-11935-9. Detail
  • ABDULLA Parosh A., HOLÍK Lukáš, CHEN Yu-Fang a VOJNAR Tomáš. Mediating for reduction (on minimizing alternating Buchi automata). Theoretical Computer Science, roč. 2014, č. 552, s. 26-43. ISSN 0304-3975. Detail
  • 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. Lecture Notes in Computer Science, roč. 8413. Heidelberg: Springer Verlag, 2014, s. 412-414. ISBN 978-3-642-54861-1. Detail
  • 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. Detail
Produkty

2015

  • dWiNA - Implementace rozhodovací procedury pro WS1S, software, 2015
    Autoři: Fiedor Tomáš, Lengál Ondřej, Holík Lukáš, Vojnar Tomáš Detail
  • INCLUDER (tracer): Nástroj pro rozhodování běhové inkluze pro automaty nad daty, software, 2015
    Autoři: Rogalewicz Adam, Iosif Radu, Vojnar Tomáš Detail

2014

  • HADES (Hazard Detection System), software, 2014
    Autoři: Charvát Lukáš, Smrčka Aleš, Vojnar Tomáš Detail
  • SLIDE: Separační logika s induktivními definicemi, software, 2014
    Autoři: Rogalewicz Adam, Iosif Radu, Vojnar Tomáš Detail
  • SPEN - Rozhodovací procedura pro separační logiku, software, 2014
    Autoři: Enea Constantin, Lengál Ondřej, Sighireanu Mihaela, Vojnar Tomáš Detail
Nahoru