Detail projektu
Statická a dynamická verifikace programů s pokročilými rysy paralelismu a neomezenosti
Období řešení: 1. 1. 2010 - 31. 12. 2013
Typ projektu: grant
Kód: GAP103/10/0306
Agentura: Grantová agentura České republiky
Program: Standardní projekty
automatická verifikace programů; statická a dynamická analýza; formální verifikace; model checking; paralelismus; nekonečně stavové programy; dynamické datové struktury
Automatizovaná verifikace programů je v současnosti s ohledem na rostoucí dopad počítačem řízených systémů na naše životy a výraznou potřebu minimalizovat počet chyb v těchto systémech velmi aktuálním výzkumným tématem. Projekt se konkrétně zaměřuje na verifikaci programů s pokročilými rysy paralelismu a neomezenosti, které patří k obzvláště problematickým aspektům software, se kterými se musí automatická verifikace vyrovnávat. V prvním případě se projekt soustřeďuje zejména na metody verifikace programů určených pro moderní vícejádrové procesory. V druhém případě se jedná o verifikaci programů pracujících s různými neomezenými datovými strukturami, zejména pak poli (o parametrické velikosti) a složitými dynamickými strukturami založenými na ukazatelích (jako jsou seznamy či stromy). Projekt zahrnuje výzkum metod dynamické i statické verifikace, včetně model checkingu, a také jejích vhodných kombinací. Pro práci s programy s nekonečnými stavovými prostory se výzkum v projektu zaměřuje na metody efektivní symbolické verifikace založené na použití automatů a logik.
Č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)
Hýsek Jiří, Ing. (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)
2015
- FIEDOR Jan, DUDKA Vendula, KŘENA Bohuslav, LETKO Zdeněk, UR Shmuel a VOJNAR Tomáš. Advances in Noise-based Testing of Concurrent Programs. Software Testing, Verification and Reliability, roč. 25, č. 3, 2015, s. 272-309. ISSN 1099-1689. Detail
2013
- ABDULLA Parosh A., HAZIZA Frédéric a HOLÍK Lukáš. All for the Price of Few (Parameterized Verification through View Abstraction). In: Proc. of VMCAI 2013. Berlin Heidelberg: Springer Verlag, 2013, s. 476-495. ISBN 978-3-642-35872-2. ISSN 0302-9743. Detail
- CHARVÁT Lukáš, SMRČKA Aleš a VOJNAR Tomáš. An Abstraction of Multi-Port Memories with Arbitrary Addressable Units. In: Computer Aided Systems Theory - EUROCAST 2013. Lecture Notes in Computer Science, roč. 8111. Berlin Heidelberg: Springer Verlag, 2013, s. 460-468. ISBN 978-3-642-53855-1. Detail
- ABDULLA Parosh A., HAZIZA Frédéric, HOLÍK Lukáš, JONSSON Bengt a REZINE Ahmed. An Integrated Specification and Verification Technique for Highly Concurrent Data Structures. In: 19th International Conference, TACAS 2013. Lecture Notes in Computer Science, roč. 7795. Berlin Heidelberg: Springer Verlag, 2013, s. 324-338. ISBN 978-3-642-36742-7. ISSN 0302-9743. Detail
- LETKO Zdeněk. Analysis and Testing of Concurrent Programs. Information Sciences and Technologies Bulletin of the ACM Slovakia, roč. 5, č. 3, 2013, s. 1-8. ISSN 1338-1237. Detail
- IOSIF Radu a ROGALEWICZ Adam. Automata-Based Termination Proofs. Computing and Informatics, roč. 2013, č. 4, s. 739-775. ISSN 1335-9150. Detail
- 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
- DUDKA Kamil, PERINGER Petr a VOJNAR Tomáš. Byte-Precise Verification of Low-Level List Manipulation. In: 20th Static Analysis Symposium. Lecture Notes in Computer Science Volume 7935, roč. 20. Berlin: Springer Verlag, 2013, s. 215-237. ISBN 978-3-642-38855-2. ISSN 0302-9743. Detail
- DUDKA Kamil, PERINGER Petr a VOJNAR Tomáš. Byte-Precise Verification of Low-Level List Manipulation. FIT-TR-2012-04, Brno: Fakulta informačních technologií VUT v Brně, 2013. Detail
- HOLÍK Lukáš, LENGÁL Ondřej, ROGALEWICZ Adam, ŠIMÁČEK Jiří a VOJNAR Tomáš. Fully Automated Shape Analysis Based on Forest Automata. In: Proceedings of CAV'13. Heidelberg: Springer Verlag, 2013, s. 740-755. ISBN 978-3-642-39798-1. ISSN 0302-9743. Detail
- HOLÍK Lukáš, LENGÁL Ondřej, ROGALEWICZ Adam, ŠIMÁČEK Jiří a VOJNAR Tomáš. Fully Automated Shape Analysis Based on Forest Automata. FIT-TR-2013-01, Brno: Fakulta informačních technologií VUT v Brně, 2013. 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
- DUDKA Kamil, MÜLLER Petr, PERINGER Petr a VOJNAR Tomáš. Predator: A Tool for Verification of Low-Level List Manipulation (Competition Contribution). In: Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science Volume 7795, roč. 2013. Berlin: Springer Verlag, 2013, s. 627-629. ISBN 978-3-642-36742-7. ISSN 0302-9743. Detail
- IOSIF Radu, ROGALEWICZ Adam a ŠIMÁČEK Jiří. The Tree Width of Separation Logic with Recursive Definitions. In: Automated Deduction - CADE-24. Lecture Notes in Artificial Intelligence, roč. 2013. Berlin: Springer Verlag, 2013, s. 21-38. ISBN 978-3-642-38573-5. ISSN 0302-9743. Detail
- IOSIF Radu, ROGALEWICZ Adam a ŠIMÁČEK Jiří. The Tree Width of Separation Logic with Recursive Definitions. arXiv:1301.5139, 2013. 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. In: Proceedings of ATVA'13. Heidelberg: Springer Verlag, 2013, s. 224-239. ISBN 978-3-319-02443-1. 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. FIT-TR-2013-02, Brno: Fakulta informačních technologií VUT v Brně, 2013. 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
- LENGÁL Ondřej. An Efficient Finite Tree Automata Library: The Design of BDD-based Semi-symbolic Algorithms for Nondeterministic Finite Tree Automata. Saarbrücken: Lambert Academic Publishing, 2012. ISBN 978-3-659-27069-7. 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
- NOVOSAD Petr a ČEŠKA Milan. Unfoldings of Bounded Hybrid Petri Nets. Lecture Notes in Computer Science, roč. 2012, č. 6927, s. 543-550. 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
- 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
- KŘENA Bohuslav, LETKO Zdeněk, VOJNAR Tomáš a UR Shmuel. A Platform for Search-Based Testing of Concurrent Software. 6th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science. Brno: Masarykova universita, 2010. ISBN 978-80-87342-10-7. 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
- LETKO Zdeněk. Sophisticated Testing of Concurrent Software. In: SSBSE '10. Proceedings of 2nd International Symposium on Search Based Software Engineering. Benevento: Institute of Electrical and Electronics Engineers, 2010, s. 36-40. ISBN 978-0-7695-4195-2. Detail
- SMRČKA Aleš a VOJNAR Tomáš. Verification of Asynchronous and Parametrized Hardware Designs. FIT Monograph. Brno: Fakulta informačních technologií VUT v Brně, 2010. ISBN 978-80-214-4214-6. Detail
- SMRČKA Aleš. Verification of Asynchronous and Parametrized Hardware Designs. Information Sciences and Technologies Bulletin of the ACM Slovakia, roč. 2, č. 2, 2010, s. 60-69. ISSN 1338-1237. 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
2013
- CPAlien: Konfigurovatelná analýza programů nad symbolickými paměťovými grafy, software, 2013
Autoři: Müller Petr, Vojnar Tomáš Detail
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 - Framework pro formální verifikaci asynchronních komponent, software, 2010
Autoři: Smrčka Aleš, Vojnar Tomáš Detail - libSFTA: Prototyp knihovny pro efektivní práci se semi-symbolicky reprezentovanými nedeterministickými stromovými automaty, software, 2010
Autoři: Holík Lukáš, Lengál Ondřej, 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