Prof. Ing. Tomáš Vojnar, Ph.D.

Static and Dynamic Verification of Programs with Advanced Features of Concurrency and Unboundedness

Czech title:Statická a dynamická verifikace programů s pokročilými rysy paralelismu a neomezenosti
Reseach leader:Vojnar Tomáš
Team leaders:Češka Milan, Křena Bohuslav, Peringer Petr, Rogalewicz Adam, Smrčka Aleš
Team members:Dudka Kamil, Dudka Vendula, Fiedor Jan, Gach Marek, Holík Lukáš, Hýsek Jiří, Charvát Lukáš, Konečný Filip, Letko Zdeněk, Šimáček Jiří
Agency:Czech Science Foundation
Code:GAP103/10/0306
Start:2010-01-01
End:2013-12-31
Keywords:automated verification of programs; static and dynamic analysis; formal verification; model checking; concurrency; infinite-state programs; dynamic data structures
Annotation:
Automated verification of programs is currently a very hot issue due to the rising influence of computer-controlled systems on our lives and the recognised need to minimise the number of errors in them. The project, in particular, considers verification of programs with advanced features of concurrency and unboundedness, which both belong among especially problematic features to be dealt with in automated verification. In the former case, the project pays a special attention to verification of applications intended to run on the current multi-core processors. In the latter case, verification of programs manipulating different unbounded structures, notably (parametrised-size) arrays and complex dynamic linked data structures (such as lists or trees), is considered. The project contains research on methods of dynamic as well as static verification, including model checking, and possibly their suitable combinations. For handling infinite-state programs, efficient symbolic verification methods based on automata and logics are the primary target of the research in the project.

Products

2013CPAlien: Configurable Program Analysis over Symbolic Memory Graphs, software, 2013
Authors: Müller Petr, Vojnar Tomáš
2012A Framework for Analysing Multi-threaded C/C++ Programs on the Binary Level, software, 2012
Authors: Fiedor Jan, Vojnar Tomáš
 HAVEN: An Open Framework for FPGA-Accelerated Functional Verification of Hardware, software, 2012
Authors: Zachariášová Marcela, Lengál Ondřej, Kajan Michal
 VATA: A Library for Efficient Manipulation of Non-Deterministic Tree Automata, software, 2012
Authors: Lengál Ondřej, Šimáček Jiří, Vojnar Tomáš
2011A Tool Chain Combining Dynamic Analysis and Bounded Model Checking, software, 2011
Authors: Dudka Vendula, Fiedor Jan, Křena Bohuslav, Vojnar Tomáš
2010An Easy to Use Infrastructure for Building Static Analysis Tools, software, 2010
Authors: Dudka Kamil, Peringer Petr, Vojnar Tomáš
 Forester: A Tool for Verification of Programs with Pointers, software, 2010
Authors: Habermehl Peter, Holík Lukáš, Rogalewicz Adam, Šimáček Jiří, Vojnar Tomáš
 Framework for Formal Verification of Clock Domain Crossing, software, 2010
Authors: Smrčka Aleš, Vojnar Tomáš
 libSFTA: A Semi-symbolic Nondeterministic Finite Tree Automata Library Prototype, software, 2010
Authors: Holík Lukáš, Lengál Ondřej, Vojnar Tomáš
 Predator: A Tool for Checking Manipulation of Dynamic Data Structures Using Separation Logic, software, 2010
Authors: Dudka Kamil, Peringer Petr, Vojnar Tomáš
 Replay Tracer & BMC, software, 2010
Authors: Dudka Vendula, Fiedor Jan, Křena Bohuslav, Letko Zdeněk, Vojnar Tomáš
 Search-based Testing Environment (SearchBestie), software, 2010
Authors: Letko Zdeněk, Vojnar Tomáš, Křena Bohuslav
 Tool for verification of systems described using the Modechart formalism, software, 2010
Authors: Gach Marek, Fiedor Jan, Češka Milan
 Tool for verification of systems specified in RT-Logic language, software, 2010
Authors: Fiedor Jan, Gach Marek, Češka Milan

Publications

2015FIEDOR Jan, DUDKA Vendula, KŘENA Bohuslav, LETKO Zdeněk, UR Shmuel and VOJNAR Tomáš. Advances in Noise-based Testing of Concurrent Programs. Software Testing, Verification and Reliability. 2015, vol. 25, no. 3, pp. 272-309. ISSN 1099-1689.
2013ABDULLA Parosh A., CEDERBERG Jonathan and VOJNAR Tomáš. Monotonic Abstraction for Programs with Multiply-Linked Structures. International Journal of Foundations of Computer Science. 2013, vol. 24, no. 2, pp. 187-210. ISSN 0129-0541.
 ABDULLA Parosh A., HAZIZA Frédéric and HOLÍK Lukáš. All for the Price of Few (Parameterized Verification through View Abstraction). In: Proc. of VMCAI 2013. Berlin Heidelberg: Springer Verlag, 2013, pp. 476-495. ISBN 978-3-642-35872-2. ISSN 0302-9743.
 ABDULLA Parosh A., HAZIZA Frédéric, HOLÍK Lukáš, JONSSON Bengt and REZINE Ahmed. An Integrated Specification and Verification Technique for Highly Concurrent Data Structures. In: 19th International Conference, TACAS 2013. Berlin Heidelberg: Springer Verlag, 2013, pp. 324-338. ISBN 978-3-642-36742-7. ISSN 0302-9743.
 ABDULLA Parosh A., HOLÍK Lukáš, JONSSON Bengt, LENGÁL Ondřej, TRINH Quy Cong and VOJNAR Tomáš. Verification of Heap Manipulating Programs with Ordered Data by Extended Forest Automata. FIT-TR-2013-02, Brno: Faculty of Information Technology BUT, 2013.
 ABDULLA Parosh A., HOLÍK Lukáš, JONSSON Bengt, LENGÁL Ondřej, TRINH Quy Cong and VOJNAR Tomáš. Verification of Heap Manipulating Programs with Ordered Data by Extended Forest Automata. In: Proceedings of ATVA'13. Heidelberg: Springer Verlag, 2013, pp. 224-239. ISBN 978-3-319-02443-1.
 CHARVÁT Lukáš, SMRČKA Aleš and VOJNAR Tomáš. An Abstraction of Multi-Port Memories with Arbitrary Addressable Units. In: Computer Aided Systems Theory - EUROCAST 2013. Berlin Heidelberg: Springer Verlag, 2013, pp. 460-468. ISBN 978-3-642-53855-1.
 DUDKA Kamil, MÜLLER Petr, PERINGER Petr and 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. Berlin: Springer Verlag, 2013, pp. 627-629. ISBN 978-3-642-36742-7. ISSN 0302-9743.
 DUDKA Kamil, PERINGER Petr and VOJNAR Tomáš. Byte-Precise Verification of Low-Level List Manipulation. FIT-TR-2012-04, Brno: Faculty of Information Technology BUT, 2013.
 DUDKA Kamil, PERINGER Petr and VOJNAR Tomáš. Byte-Precise Verification of Low-Level List Manipulation. In: 20th Static Analysis Symposium. Berlin: Springer Verlag, 2013, pp. 215-237. ISBN 978-3-642-38855-2. ISSN 0302-9743.
 HOLÍK Lukáš, LENGÁL Ondřej, ROGALEWICZ Adam, ŠIMÁČEK Jiří and VOJNAR Tomáš. Fully Automated Shape Analysis Based on Forest Automata. FIT-TR-2013-01, Brno: Faculty of Information Technology BUT, 2013.
 HOLÍK Lukáš, LENGÁL Ondřej, ROGALEWICZ Adam, ŠIMÁČEK Jiří and VOJNAR Tomáš. Fully Automated Shape Analysis Based on Forest Automata. In: Proceedings of CAV'13. Heidelberg: Springer Verlag, 2013, pp. 740-755. ISBN 978-3-642-39798-1. ISSN 0302-9743.
 IOSIF Radu and ROGALEWICZ Adam. Automata-Based Termination Proofs. Computing and Informatics. Bratislava: Slovak Academic Press, 2013, vol. 2013, no. 4, pp. 739-775. ISSN 1335-9150.
 IOSIF Radu, ROGALEWICZ Adam and ŠIMÁČEK Jiří. The Tree Width of Separation Logic with Recursive Definitions. arXiv:1301.5139, 2013.
 IOSIF Radu, ROGALEWICZ Adam and ŠIMÁČEK Jiří. The Tree Width of Separation Logic with Recursive Definitions. In: Automated Deduction - CADE-24. Berlin: Springer Verlag, 2013, pp. 21-38. ISBN 978-3-642-38573-5. ISSN 0302-9743.
 KŘENA Bohuslav and VOJNAR Tomáš. Automated formal analysis and verification: an overview. International Journal of General Systems. Abingdon: Taylor & Francis Informa plc, 2013, vol. 2013, no. 42, pp. 335-365. ISSN 0308-1079.
 LETKO Zdeněk. Analysis and Testing of Concurrent Programs. Information Sciences and Technologies Bulletin of the ACM Slovakia. Bratislava: Vydavateľstvo STU, 2013, vol. 5, no. 3, pp. 1-8. ISSN 1338-1237.
2012BOUAJJANI Ahmed, HABERMEHL Peter, ROGALEWICZ Adam and VOJNAR Tomáš. Abstract Regular (Tree) Model Checking. International Journal on Software Tools for Technology Transfer. 2012, vol. 14, no. 2, pp. 167-191. ISSN 1433-2779.
 CHARVÁT Lukáš, SMRČKA Aleš and 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, pp. 6-12. ISBN 978-1-4673-4441-8.
 DUDKA Kamil, MÜLLER Petr, PERINGER Petr and VOJNAR Tomáš. Predator: A Verification Tool for Programs with Dynamic Linked Data Structures. Lecture Notes in Computer Science. 2012, vol. 2012, no. 7214, pp. 544-547. ISSN 0302-9743.
 DUDKA Kamil, PERINGER Petr and VOJNAR Tomáš. An Easy to Use Infrastructure for Building Static Analysis Tools. Lecture Notes in Computer Science. 2012, vol. 2012, no. 6927, pp. 527-534. ISSN 0302-9743.
 DUDKA Vendula, FIEDOR Jan, KŘENA Bohuslav and VOJNAR Tomáš. DA-BMC: A Tool Chain Combining Dynamic Analysis and Bounded Model Checking. Lecture Notes in Computer Science. 2012, vol. 2012, no. 7186, p. 5. ISSN 0302-9743.
 DUDKA Vendula, KŘENA Bohuslav, LETKO Zdeněk and VOJNAR Tomáš. Testing of Concurrent Programs Using Genetic Algorithms. FIT-TR-2012-01, Brno, 2012.
 DUDKA Vendula, KŘENA Bohuslav, LETKO Zdeněk, UR Shmuel and VOJNAR Tomáš. Testing of Concurrent Programs with Genetic Algorithms. Lecture Notes in Computer Science. 2012, vol. 2012, no. 7515, pp. 152-167. ISSN 0302-9743.
 FIEDOR Jan and VOJNAR Tomáš. ANaConDA: A Framework for Analysing Multi-threaded C/C++ Programs on the Binary Level. Lecture Notes in Computer Science. 2012, vol. 2012, no. 7687, pp. 35-41. ISSN 0302-9743.
 FIEDOR Jan and VOJNAR Tomáš. Noise-Based Testing and Analysis of Multi-threaded C/C++ Programs on the Binary Level. In: PADTAD '12. New York: Association for Computing Machinery, 2012, pp. 36-46. ISBN 978-1-4503-1456-5.
 FIEDOR Jan, KŘENA Bohuslav, LETKO Zdeněk and VOJNAR Tomáš. A Uniform Classification of Common Concurrency Errors. Lecture Notes in Computer Science. 2012, vol. 2012, no. 6927, pp. 519-526. ISSN 0302-9743.
 HABERMEHL Peter, HOLÍK Lukáš, ROGALEWICZ Adam, ŠIMÁČEK Jiří and VOJNAR Tomáš. Forest Automata for Verification of Heap Manipulation. Formal Methods in System Design. Berlin: Springer Verlag, 2012, vol. 2012, no. 41, pp. 83-106. ISSN 0925-9856.
 IOSIF Radu, HOJJAT Hossein, KONEČNÝ Filip, KUNCAK Viktor and RUMMER Philipp. Accelerating Interpolants. Lecture Notes in Computer Science. 2012, vol. 2012, no. 7561, pp. 187-202. ISSN 0302-9743.
 KONEČNÝ Filip, HOJJAT Hossein, IOSIF Radu, KUNCAK Viktor, RUMMER Philipp and GARNIER Florent. A Verification Toolkit for Numerical Transition Systems. Lecture Notes in Computer Science. 2012, vol. 2012, no. 7436, pp. 247-251. ISSN 0302-9743.
 KONEČNÝ Filip, IOSIF Radu and BOZGA Marius. Deciding Conditional Termination. Lecture Notes in Computer Science. 2012, vol. 2012, no. 7214, pp. 252-266. ISSN 0302-9743.
 KŘENA Bohuslav, LETKO Zdeněk and VOJNAR Tomáš. Analysis and Testing of Concurrent Programs. Brno: Faculty of Information Technology BUT, 2012. ISBN 978-80-214-4464-5.
 KŘENA Bohuslav, LETKO Zdeněk and VOJNAR Tomáš. Coverage Metrics for Saturation-based and Search-based Testing of Concurrent Software. Lecture Notes in Computer Science. 2012, vol. 2012, no. 7186, pp. 177-192. ISSN 0302-9743.
 KŘENA Bohuslav, LETKO Zdeněk and VOJNAR Tomáš. Noise Injection Heuristics for Concurrency Testing. Lecture Notes in Computer Science. 2012, vol. 2012, no. 7119, pp. 123-131. ISSN 0302-9743.
 LENGÁL Ondřej, ŠIMÁČEK Jiří and VOJNAR Tomáš. VATA: A Library for Efficient Manipulation of Non-Deterministic Tree Automata. Lecture Notes in Computer Science. 2012, vol. 2012, no. 7214, pp. 79-94. ISSN 0302-9743.
 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.
 NOVOSAD Petr and ČEŠKA Milan. Unfoldings of Bounded Hybrid Petri Nets. Lecture Notes in Computer Science. 2012, vol. 2012, no. 6927, pp. 543-550. ISSN 0302-9743.
 ZACHARIÁŠOVÁ Marcela, LENGÁL Ondřej and KAJAN Michal. HAVEN: An Open Framework for FPGA-Accelerated Functional Verification of Hardware. Lecture Notes in Computer Science. 2012, vol. 2012, no. 7261, pp. 247-253. ISSN 0302-9743.
 ČEŠKA Milan, FIEDOR Jan and GACH Marek. A Novel Approach to Modechart Verification of Real-Time systems. Lecture Notes in Computer Science. 2012, vol. 2012, no. 6927, pp. 559-567. ISSN 0302-9743.
2011ABDULLA Parosh A., CHEN Yu-Fang, CLEMENTE Lorenzo, HOLÍK Lukáš, HONG Chih-Duo, MAYR Richard and VOJNAR Tomáš. Advanced Ramsey-based Büchi Automata Inclusion Testing. FIT-TR-2011-03, Brno: Faculty of Information Technology BUT, 2011.
 ABDULLA Parosh A., CHEN Yu-Fang, CLEMENTE Lorenzo, HOLÍK Lukáš, HONG Chih-Duo, MAYR Richard and VOJNAR Tomáš. Advanced Ramsey-based Büchi Automata Inclusion Testing. Lecture Notes in Computer Science. 2011, vol. 2011, no. 6901, pp. 187-202. ISSN 0302-9743.
 BOUAJJANI Ahmed, BOZGA Marius, HABERMEHL Peter, IOSIF Radu, MORO Pierre and VOJNAR Tomáš. Programs with Lists are Counter Automata. Formal Methods in System Design. Berlin: Springer Verlag, 2011, vol. 38, no. 2, pp. 158-192. ISSN 0925-9856.
 DUDKA Kamil, PERINGER Petr and VOJNAR Tomáš. Predator: A Practical Tool for Checking Manipulation of Dynamic Data Structures Using Separation Logic. FIT-TR-2011-02, Brno: Faculty of Information Technology BUT, 2011.
 DUDKA Kamil, PERINGER Petr and 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: The Universidad de Las Palmas de Gran Canaria, 2011, pp. 328-329. ISBN 978-84-693-9560-8.
 DUDKA Kamil, PERINGER Petr and VOJNAR Tomáš. Predator: A Practical Tool for Checking Manipulation of Dynamic Data Structures Using Separation Logic. Lecture Notes in Computer Science. 2011, vol. 2011, no. 6806, pp. 372-378. ISSN 0302-9743.
 DUDKA Vendula, FIEDOR Jan, KŘENA Bohuslav and VOJNAR Tomáš. DA-BMC: A Tool Chain Combining Dynamic Analysis and Bounded Model Checking. FIT-TR-2011-06, Brno: Faculty of Information Technology BUT, 2011.
 FIEDOR Jan, KŘENA Bohuslav, LETKO Zdeněk and 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: The Universidad de Las Palmas de Gran Canaria, 2011, pp. 326-327. ISBN 978-84-693-9560-8.
 HABERMEHL Peter, HOLÍK Lukáš, ROGALEWICZ Adam, ŠIMÁČEK Jiří and VOJNAR Tomáš. Forest Automata for Verification of Heap Manipulation. FIT-TR-2011-01, Brno: Faculty of Information Technology BUT, 2011.
 HABERMEHL Peter, HOLÍK Lukáš, ROGALEWICZ Adam, ŠIMÁČEK Jiří and VOJNAR Tomáš. Forest Automata for Verification of Heap Manipulation. Lecture Notes in Computer Science. 2011, vol. 2011, no. 6806, pp. 424-440. ISSN 0302-9743.
 HOLÍK Lukáš, LENGÁL Ondřej, ŠIMÁČEK Jiří and VOJNAR Tomáš. Efficient Inclusion Checking on Explicit and Semi-Symbolic Tree Automata. FIT-TR-2011-04, Brno: Faculty of Information Technology BUT, 2011.
 HOLÍK Lukáš, LENGÁL Ondřej, ŠIMÁČEK Jiří and VOJNAR Tomáš. Efficient Inclusion Checking on Explicit and Semi-Symbolic Tree Automata. Lecture Notes in Computer Science. 2011, vol. 2011, no. 6996, pp. 243-258. ISSN 0302-9743.
 ZACHARIÁŠOVÁ Marcela, LENGÁL Ondřej and KAJAN Michal. HAVEN: An Open Framework for FPGA-Accelerated Functional Verification of Hardware. FIT-TR-2011-05, Brno: Faculty of Information Technology BUT, 2011.
 ČEŠKA Milan, FIEDOR Jan and 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: The Universidad de Las Palmas de Gran Canaria, 2011, pp. 338-339. ISBN 978-84-693-9560-8.
2010ABDULLA Parosh A., CLEMENTE Lorenzo, HOLÍK Lukáš, HONG Chih-Duo, CHEN Yu-Fang, MAYR Richard and VOJNAR Tomáš. Simulation Subsumption in Ramsey-based Büchi Automata Universality and Inclusion Testing. FIT-TR-2010-02, Brno: Faculty of Information Technology BUT, 2010.
 ABDULLA Parosh A., CLEMENTE Lorenzo, HOLÍK Lukáš, HONG Chih-Duo, CHEN Yu-Fang, MAYR Richard and VOJNAR Tomáš. Simulation Subsumption in Ramsey-Based Büchi Automata Universality and Inclusion Testing. In: Computer Aided Verification. Berlín: Springer Verlag, 2010, pp. 132-147. ISBN 978-3-642-14294-9.
 ABDULLA Parosh A., HOLÍK Lukáš, CHEN Yu-Fang, MAYR Richard and 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. Berlín: Springer Verlag, 2010, pp. 158-174. ISBN 978-3-642-12001-5.
 BOZGA Marius, IOSIF Radu and KONEČNÝ Filip. Fast Acceleration of Ultimately Periodic Relations. In: Computer Aided Verification. Berlin: Springer Verlag, 2010, pp. 227-242. ISBN 978-3-642-14294-9.
 FIEDOR Jan, KŘENA Bohuslav, LETKO Zdeněk and VOJNAR Tomáš. A Uniform Classification of Common Concurrency Errors. FIT-TR-2010-03, Brno, 2010.
 HOLÍK Lukáš and VOJNAR Tomáš. Simulations and Aintichains for Efficient Handling of Tree Automata. Brno: Faculty of Information Technology BUT, 2010. ISBN 978-80-214-4217-7.
 KŘENA Bohuslav, LETKO Zdeněk, UR Shmuel and VOJNAR Tomáš. A Platform for Search-Based Testing of Concurrent Software. In: PADTAD '10. Trento: Association for Computing Machinery, 2010, p. 11. ISBN 978-1-60558-823-0.
 KŘENA Bohuslav, LETKO Zdeněk, VOJNAR Tomáš and UR Shmuel. A Platform for Search-Based Testing of Concurrent Software. 6th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science. Brno: Masaryk University, 2010. ISBN 978-80-87342-10-7.
 LETKO Zdeněk. Sophisticated Testing of Concurrent Programs. In: SSBSE '10. Benevento: Institute of Electrical and Electronics Engineers, 2010, pp. 36-40. ISBN 978-0-7695-4195-2.
 SMRČKA Aleš and VOJNAR Tomáš. Verification of Asynchronous and Parametrized Hardware Designs. Brno: Faculty of Information Technology BUT, 2010. ISBN 978-80-214-4214-6.
 SMRČKA Aleš. Verification of Asynchronous and Parametrized Hardware Designs. Information Sciences and Technologies Bulletin of the ACM Slovakia. Bratislava: Vydavateľstvo STU, 2010, vol. 2, no. 2, pp. 60-69. ISSN 1338-1237.

Your IPv4 address: 54.82.81.154
Switch to IPv6 connection

DNSSEC [dnssec]