Detail projektu

Práce se složitými datovými strukturami a paralelismem v prostředí Rich Model Toolkit

Období řešení: 1. 1. 2010 - 31. 12. 2012

Typ projektu: grant

Kód: OC10009

Agentura: Ministerstvo školství, mládeže a tělovýchovy České republiky

Program: COST

Název anglicky
Dealing with Complex Data Structures and Concurrency within the Rich Model Toolkit
Typ
grant
Klíčová slova

automatizovaná verifikace, programy se složitými datovými strukturami, paralelní systémy, symbolická verifikace, statická a dynamická analýza, model checking, teorie automatů a logik

Abstrakt

Projekt je příspěvkem k výzkumu realizovanému v rámci COST akce IC0901: Rich Model Toolkit - An Infrastructure for Reliable Computer Systems, zaměřené (1) na vývoj jazyka pro homogenní popis co nejširšího spektra počítačových systémů pro potřeby jejich následné verifikace a (2) na výzkum v oblasti metod formální verifikace s cílem výrazně zvýšit míru jejich obecnosti, efektivnosti a stupně automatizace. Výzkum v projektu se konkrétně zaměří na dva aspekty chování počítačových systémů představující významnou výzvu pro současné verifikační přístupy, a to na práci se složitými datovými strukturami (včetně dynamických datových struktur založených na ukazatelích) a na použití paralelismu v moderních počítačových systémech. V prvním případě se bude jednat zejména o výzkum metod symbolické verifikace založených na aplikacích teorie automatů, logik a jejich kombinací. V druhém případě pak o výzkum v oblasti model checkingu, statické analýzy, dynamické analýzy i jejich vhodných kombinací s cílem dosáhnout tímto způsobem významného zlepšení možností verifikace současných masivně paralelních systémů.

Řešitelé
Vojnar Tomáš, prof. Ing., Ph.D. (UITS FIT VUT) , hlavní řešitel
Češka Milan, prof. RNDr., CSc. (UITS FIT VUT) , spoluřešitel
Křena Bohuslav, Ing., Ph.D. (UITS FIT VUT) , spoluřešitel
Peringer Petr, Dr. Ing. (UITS FIT VUT) , spoluřešitel
Rogalewicz Adam, doc. Mgr., Ph.D. (UITS FIT VUT) , spoluřešitel
Smrčka Aleš, Ing., Ph.D. (UITS FIT VUT) , spoluřešitel
Dudka Kamil, Ing. (UITS FIT VUT)
Dudka Vendula, Ing. (UITS FIT VUT)
Fiedor Jan, Ing., Ph.D. (UITS FIT VUT)
Gach Marek, Ing. (UITS FIT VUT)
Holík Lukáš, doc. Mgr., Ph.D. (UITS FIT VUT)
Charvát Lukáš, Ing. (UITS FIT VUT)
Konečný Filip, Ing. (UITS FIT VUT)
Letko Zdeněk, Ing., Ph.D. (UITS FIT VUT)
Šimáček Jiří, Ing., Ph.D. (UITS FIT VUT)
Publikace

2013

  • KŘENA Bohuslav a VOJNAR Tomáš. Automated formal analysis and verification: an overview. International Journal of General Systems, roč. 2013, č. 42, s. 335-365. ISSN 0308-1079. Detail
  • ABDULLA Parosh A., CEDERBERG Jonathan a VOJNAR Tomáš. Monotonic Abstraction for Programs with Multiply-Linked Structures. International Journal of Foundations of Computer Science, roč. 24, č. 2, 2013, s. 187-210. ISSN 0129-0541. Detail

2012

  • ČEŠKA Milan, FIEDOR Jan a GACH Marek. A Novel Approach to Modechart Verification of Real-Time systems. Lecture Notes in Computer Science, roč. 2012, č. 6927, s. 559-567. ISSN 0302-9743. Detail
  • FIEDOR Jan, KŘENA Bohuslav, LETKO Zdeněk a VOJNAR Tomáš. A Uniform Classification of Common Concurrency Errors. Lecture Notes in Computer Science, roč. 2012, č. 6927, s. 519-526. ISSN 0302-9743. Detail
  • KONEČNÝ Filip, HOJJAT Hossein, IOSIF Radu, KUNCAK Viktor, RUMMER Philipp a GARNIER Florent. A Verification Toolkit for Numerical Transition Systems. Lecture Notes in Computer Science, roč. 2012, č. 7436, s. 247-251. ISSN 0302-9743. Detail
  • BOUAJJANI Ahmed, HABERMEHL Peter, ROGALEWICZ Adam a VOJNAR Tomáš. Abstract Regular (Tree) Model Checking. International Journal on Software Tools for Technology Transfer, roč. 14, č. 2, 2012, s. 167-191. ISSN 1433-2779. Detail
  • IOSIF Radu, HOJJAT Hossein, KONEČNÝ Filip, KUNCAK Viktor a RUMMER Philipp. Accelerating Interpolants. Lecture Notes in Computer Science, roč. 2012, č. 7561, s. 187-202. ISSN 0302-9743. Detail
  • DUDKA Kamil, PERINGER Petr a VOJNAR Tomáš. An Easy to Use Infrastructure for Building Static Analysis Tools. Lecture Notes in Computer Science, roč. 2012, č. 6927, s. 527-534. ISSN 0302-9743. Detail
  • FIEDOR Jan a VOJNAR Tomáš. ANaConDA: A Framework for Analysing Multi-threaded C/C++ Programs on the Binary Level. Lecture Notes in Computer Science, roč. 2012, č. 7687, s. 35-41. ISSN 0302-9743. Detail
  • KŘENA Bohuslav, LETKO Zdeněk a VOJNAR Tomáš. Analysis and Testing of Concurrent Programs. FIT Monograph. Brno: Fakulta informačních technologií VUT v Brně, 2012. ISBN 978-80-214-4464-5. Detail
  • CHARVÁT Lukáš, SMRČKA Aleš a VOJNAR Tomáš. Automatic Formal Correspondence Checking of ISA and RTL Microprocessor Description. In: Proceedings of the 13th International Workshop on Microprocessor Test and Verification (MTV 2012). Austin, TX: Institute of Electrical and Electronics Engineers, 2012, s. 6-12. ISBN 978-1-4673-4441-8. Detail
  • KŘENA Bohuslav, LETKO Zdeněk a VOJNAR Tomáš. Coverage Metrics for Saturation-based and Search-based Testing of Concurrent Software. Lecture Notes in Computer Science, roč. 2012, č. 7186, s. 177-192. ISSN 0302-9743. Detail
  • DUDKA Vendula, FIEDOR Jan, KŘENA Bohuslav a VOJNAR Tomáš. DA-BMC: A Tool Chain Combining Dynamic Analysis and Bounded Model Checking. Lecture Notes in Computer Science, roč. 2012, č. 7186, s. 5. ISSN 0302-9743. Detail
  • KONEČNÝ Filip, IOSIF Radu a BOZGA Marius. Deciding Conditional Termination. Lecture Notes in Computer Science, roč. 2012, č. 7214, s. 252-266. ISSN 0302-9743. Detail
  • HABERMEHL Peter, HOLÍK Lukáš, ROGALEWICZ Adam, ŠIMÁČEK Jiří a VOJNAR Tomáš. Forest Automata for Verification of Heap Manipulation. Formal Methods in System Design, roč. 2012, č. 41, s. 83-106. ISSN 0925-9856. Detail
  • ZACHARIÁŠOVÁ Marcela, LENGÁL Ondřej a KAJAN Michal. HAVEN: An Open Framework for FPGA-Accelerated Functional Verification of Hardware. Lecture Notes in Computer Science, roč. 2012, č. 7261, s. 247-253. ISSN 0302-9743. Detail
  • KŘENA Bohuslav, LETKO Zdeněk a VOJNAR Tomáš. Noise Injection Heuristics for Concurrency Testing. Lecture Notes in Computer Science, roč. 2012, č. 7119, s. 123-131. ISSN 0302-9743. Detail
  • FIEDOR Jan a VOJNAR Tomáš. Noise-Based Testing and Analysis of Multi-threaded C/C++ Programs on the Binary Level. In: PADTAD '12. Proceedings of the 10th Workshop on Parallel and Distributed Systems. New York: Association for Computing Machinery, 2012, s. 36-46. ISBN 978-1-4503-1456-5. Detail
  • DUDKA Kamil, MÜLLER Petr, PERINGER Petr a VOJNAR Tomáš. Predator: A Verification Tool for Programs with Dynamic Linked Data Structures (Competition Contribution). Lecture Notes in Computer Science, roč. 2012, č. 7214, s. 544-547. ISSN 0302-9743. Detail
  • DUDKA Vendula, KŘENA Bohuslav, LETKO Zdeněk a VOJNAR Tomáš. Testing of Concurrent Programs Using Genetic Algorithms. FIT-TR-2012-01, Brno, 2012. Detail
  • DUDKA Vendula, KŘENA Bohuslav, LETKO Zdeněk, UR Shmuel a VOJNAR Tomáš. Testování vícevláknových aplikací pomocí genetických algoritmů. Lecture Notes in Computer Science, roč. 2012, č. 7515, s. 152-167. ISSN 0302-9743. Detail
  • LENGÁL Ondřej, ŠIMÁČEK Jiří a VOJNAR Tomáš. VATA: A Library for Efficient Manipulation of Non-Deterministic Tree Automata. Lecture Notes in Computer Science, roč. 2012, č. 7214, s. 79-94. ISSN 0302-9743. Detail

2011

  • ČEŠKA Milan, FIEDOR Jan a GACH Marek. A Novel Approach to Modechart Verification of Real-Time Systems. In: Proceedings of the 13th International Conference on Computer Aided Systems Theory. Universidad de Las Palmas de Canaria: Universidad de Las Palmas de Gran Canaria, 2011, s. 338-339. ISBN 978-84-693-9560-8. Detail
  • FIEDOR Jan, KŘENA Bohuslav, LETKO Zdeněk a VOJNAR Tomáš. A Uniform Classification of Common Concurrency Errors. In: Proceedings of the 13th International Conference on Computer Aided Systems Theory. Universidad de Las Palmas de Canaria: Universidad de Las Palmas de Gran Canaria, 2011, s. 326-327. ISBN 978-84-693-9560-8. Detail
  • ABDULLA Parosh A., CHEN Yu-Fang, CLEMENTE Lorenzo, HOLÍK Lukáš, HONG Chih-Duo, MAYR Richard a VOJNAR Tomáš. Advanced Ramsey-based Büchi Automata Inclusion Testing. FIT-TR-2011-03, Brno: Fakulta informačních technologií VUT v Brně, 2011. Detail
  • ABDULLA Parosh A., CHEN Yu-Fang, CLEMENTE Lorenzo, HOLÍK Lukáš, HONG Chih-Duo, MAYR Richard a VOJNAR Tomáš. Advanced Ramsey-based Büchi Automata Inclusion Testing. Lecture Notes in Computer Science, roč. 2011, č. 6901, s. 187-202. ISSN 0302-9743. Detail
  • DUDKA Kamil, PERINGER Petr a VOJNAR Tomáš. An Easy to Use Infrastructure for Building Static Analysis Tools. In: Proceedings of the 13th International Conference on Computer Aided Systems Theory. Universidad de Las Palmas de Canaria: Universidad de Las Palmas de Gran Canaria, 2011, s. 328-329. ISBN 978-84-693-9560-8. Detail
  • DUDKA Vendula, FIEDOR Jan, KŘENA Bohuslav a VOJNAR Tomáš. DA-BMC: A Tool Chain Combining Dynamic Analysis and Bounded Model Checking. FIT-TR-2011-06, Brno: Fakulta informačních technologií VUT v Brně, 2011. Detail
  • HOLÍK Lukáš, LENGÁL Ondřej, ŠIMÁČEK Jiří a VOJNAR Tomáš. Efficient Inclusion Checking on Explicit and Semi-Symbolic Tree Automata. Lecture Notes in Computer Science, roč. 2011, č. 6996, s. 243-258. ISSN 0302-9743. Detail
  • HOLÍK Lukáš, LENGÁL Ondřej, ŠIMÁČEK Jiří a VOJNAR Tomáš. Efficient Inclusion Checking on Explicit and Semi-Symbolic Tree Automata. FIT-TR-2011-04, Brno: Fakulta informačních technologií VUT v Brně, 2011. Detail
  • HABERMEHL Peter, HOLÍK Lukáš, ROGALEWICZ Adam, ŠIMÁČEK Jiří a VOJNAR Tomáš. Forest Automata for Verification of Heap Manipulation. Lecture Notes in Computer Science, roč. 2011, č. 6806, s. 424-440. ISSN 0302-9743. Detail
  • HABERMEHL Peter, HOLÍK Lukáš, ROGALEWICZ Adam, ŠIMÁČEK Jiří a VOJNAR Tomáš. Forest Automata for Verification of Heap Manipulation. FIT-TR-2011-01, Brno: Fakulta informačních technologií VUT v Brně, 2011. Detail
  • ZACHARIÁŠOVÁ Marcela, LENGÁL Ondřej a KAJAN Michal. HAVEN: An Open Framework for FPGA-Accelerated Functional Verification of Hardware. FIT-TR-2011-05, Brno: Fakulta informačních technologií VUT v Brně, 2011. Detail
  • ABDULLA Parosh A., CEDERBERG Jonathan a VOJNAR Tomáš. Monotonic Abstraction for Programs with Multiply-Linked Structures. Lecture Notes in Computer Science, roč. 2011, č. 6945, s. 125-138. ISSN 0302-9743. Detail
  • DUDKA Kamil, PERINGER Petr a VOJNAR Tomáš. Predator: A Practical Tool for Checking Manipulation of Dynamic Data Structures Using Separation Logic. Lecture Notes in Computer Science, roč. 2011, č. 6806, s. 372-378. ISSN 0302-9743. Detail
  • DUDKA Kamil, PERINGER Petr a VOJNAR Tomáš. Predator: A Practical Tool for Checking Manipulation of Dynamic Data Structures Using Separation Logic. FIT-TR-2011-02, Brno: Fakulta informačních technologií VUT v Brně, 2011. Detail
  • BOUAJJANI Ahmed, BOZGA Marius, HABERMEHL Peter, IOSIF Radu, MORO Pierre a VOJNAR Tomáš. Programs with Lists are Counter Automata. Formal Methods in System Design, roč. 38, č. 2, 2011, s. 158-192. ISSN 0925-9856. Detail

2010

  • KŘENA Bohuslav, LETKO Zdeněk, UR Shmuel a VOJNAR Tomáš. A Platform for Search-Based Testing of Concurrent Software. In: PADTAD '10. Proceedings of the 8th Workshop on Parallel and Distributed Systems. Trento: Association for Computing Machinery, 2010, s. 11. ISBN 978-1-60558-823-0. Detail
  • FIEDOR Jan, KŘENA Bohuslav, LETKO Zdeněk a VOJNAR Tomáš. A Uniform Classification of Common Concurrency Errors. FIT-TR-2010-03, Brno, 2010. Detail
  • BOZGA Marius, IOSIF Radu a KONEČNÝ Filip. Fast Acceleration of Ultimately Periodic Relations. In: Computer Aided Verification. Lecture Notes in Computer Science, roč. 6174. Berlin: Springer Verlag, 2010, s. 227-242. ISBN 978-3-642-14294-9. Detail
  • ABDULLA Parosh A., CLEMENTE Lorenzo, HOLÍK Lukáš, HONG Chih-Duo, CHEN Yu-Fang, MAYR Richard a VOJNAR Tomáš. Simulation Subsumption in Ramsey-based Büchi Automata Universality and Inclusion Testing. FIT-TR-2010-02, Brno: Fakulta informačních technologií VUT v Brně, 2010. Detail
  • ABDULLA Parosh A., CLEMENTE Lorenzo, HOLÍK Lukáš, HONG Chih-Duo, CHEN Yu-Fang, MAYR Richard a VOJNAR Tomáš. Simulation Subsumption in Ramsey-Based Büchi Automata Universality and Inclusion Testing. In: Computer Aided Verification. Lecture Notes in Computer Science, roč. 6174. Berlín: Springer Verlag, 2010, s. 132-147. ISBN 978-3-642-14294-9. Detail
  • HOLÍK Lukáš a VOJNAR Tomáš. Simulations and Aintichains for Efficient Handling of Tree Automata. FIT Monograph. Brno: Fakulta informačních technologií VUT v Brně, 2010. ISBN 978-80-214-4217-7. Detail
  • ABDULLA Parosh A., HOLÍK Lukáš, CHEN Yu-Fang, MAYR Richard a VOJNAR Tomáš. When Simulation Meets Antichains (On Checking Language Inclusion of Nondeterministic Finite (Tree) Automata). FIT-TR-2010-01, Brno: Fakulta informačních technologií VUT v Brně, 2010. Detail
  • ABDULLA Parosh A., HOLÍK Lukáš, CHEN Yu-Fang, MAYR Richard a VOJNAR Tomáš. When Simulation Meets Antichains (On Checking Language Inclusion of Nondeterministic Finite (Tree) Automata). In: Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, roč. 6015. Berlín: Springer Verlag, 2010, s. 158-174. ISBN 978-3-642-12001-5. Detail
Produkty

2012

  • ANaConDA: Prostředí pro analýzu vícevláknových C/C++ programů na binární úrovni, software, 2012
    Autoři: Fiedor Jan, Vojnar Tomáš Detail
  • HAVEN: Otevřený rámec pro akceleraci funkční verifikace hardwaru pomocí FPGA, software, 2012
    Autoři: Zachariášová Marcela, Lengál Ondřej, Kajan Michal Detail
  • VATA: Knihovna pro efektivní práci s nedeterministickými stromovými automaty, software, 2012
    Autoři: Lengál Ondřej, Šimáček Jiří, Vojnar Tomáš Detail

2011

  • Nástroj propojující dynamickou analýzu a bounded model checking, software, 2011
    Autoři: Dudka Vendula, Fiedor Jan, Křena Bohuslav, Vojnar Tomáš Detail

2010

  • Forester: Nástroj pro verifikaci programů s ukazateli, software, 2010
    Autoři: Habermehl Peter, Holík Lukáš, Rogalewicz Adam, Šimáček Jiří, Vojnar Tomáš Detail
  • Nástroj pro přehrávání běhu programu (Replay Tracer & BMC), software, 2010
    Autoři: Dudka Vendula, Fiedor Jan, Křena Bohuslav, Letko Zdeněk, Vojnar Tomáš Detail
  • Nástroj pro verifikaci systémů popsaných formalismem Modechart, software, 2010
    Autoři: Gach Marek, Fiedor Jan, Češka Milan Detail
  • Nástroj pro verifikaci systémů specifikovaných jazykem RT-Logiky, software, 2010
    Autoři: Fiedor Jan, Gach Marek, Češka Milan Detail
  • Predator: Nástroj pro ověřování manipulace s dynamickými datovými strukturami založený na separační logice, software, 2010
    Autoři: Dudka Kamil, Peringer Petr, Vojnar Tomáš Detail
  • Snadno použitelná infrastruktura pro výstavbu nástrojů na statickou analýzu, software, 2010
    Autoři: Dudka Kamil, Peringer Petr, Vojnar Tomáš Detail
  • Testovací prostředí využívající techniky prohledávání prostoru (SearchBestie), software, 2010
    Autoři: Letko Zdeněk, Vojnar Tomáš, Křena Bohuslav Detail
Nahoru