Prof. RNDr. Milan Češka, CSc.

Static and Dynamic Verification of Programs with Advanced Features of Concurrency and Unboundedness
Reseach leader:Vojnar Tomáš
Team leaders:Češka Milan, Křena Bohuslav, Peringer Petr, Rogalewicz Adam, Smrčka Aleš
Team members:Dudka Kamil, Fiedor Jan, Gach Marek, Holík Lukáš, Hrubá Vendula, Hýsek Jiří, Charvát Lukáš, Konečný Filip, Letko Zdeněk, Šimáček Jiří
Agency:GAČR
Code:GAP103/10/0306
Start:2010
End:2013
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

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: Šimková 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: Fiedor Jan, Hrubá Vendula, Křena Bohuslav, Vojnar Tomáš

Publications

2013Abdulla Parosh A., Haziza Frédéric, Holík Lukáš, Jonsson Bengt, Rezine Ahmed: An Integrated Specification and Verification Technique for Highly Concurrent Data Structures, In: 19th International Conference, TACAS 2013, Berlin Heidelberg, DE, Springer, 2013, p. 324-338, ISBN 978-3-642-36742-7, ISSN 0302-9743
 Abdulla Parosh A., Haziza Frédéric, Holík Lukáš: All for the Price of Few (Parameterized Verification through View Abstraction), In: Proc. of VMCAI 2013, Berlin Heidelberg, DE, Springer, 2013, p. 476-495, ISBN 978-3-642-35872-2, ISSN 0302-9743
 Dudka Kamil, Müller Petr, Peringer Petr, 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, DE, Springer, 2013, p. 627-629, ISBN 978-3-642-36742-7, ISSN 0302-9743
 Dudka Kamil, Peringer Petr, Vojnar Tomáš: Byte-Precise Verification of Low-Level List Manipulation, In: 20th Static Analysis Symposium, Berlin, DE, Springer, 2013, p. 215-237, ISBN 978-3-642-33124-4, ISSN 0302-9743
 Dudka Kamil, Peringer Petr, Vojnar Tomáš: Byte-Precise Verification of Low-Level List Manipulation, FIT-TR-2012-04, Brno, CZ, FIT VUT, 2013, p. 48
 Holík Lukáš, Lengál Ondřej, Rogalewicz Adam, Šimáček Jiří, Vojnar Tomáš: Fully Automated Shape Analysis Based on Forest Automata, In: Proceedings of CAV'13, Heidelberg, DE, Springer, 2013, p. 1-16
 Charvát Lukáš, Smrčka Aleš, Vojnar Tomáš: An Abstraction of Multi-Port Memories with Arbitrary Addressable Units, In: Proceedings of the 14th Computer Aided Systems Theory??, Las Palmas de Grand Canaria, ES, 2013, p. 1-9
 Iosif Radu, Rogalewicz Adam, Šimáček Jiří: The Tree Width of Separation Logic with Recursive Definitions, In: Proceedings of CADE-24, Berlin, DE, 2013, p. 1-18, ISSN 0302-9743
 Iosif Radu, Rogalewicz Adam, Šimáček Jiří: The Tree Width of Separation Logic with Recursive Definitions, arXiv:1301.5139, US, 2013, p. 31
 Křena Bohuslav, Vojnar Tomáš: Automated formal analysis and verification: an overview, In: International Journal of General Systems, Vol. 2013, No. 42, Abingdon, GB, p. 335-365, ISSN 0308-1079
2012Bouajjani Ahmed, Habermehl Peter, Rogalewicz Adam, Vojnar Tomáš: Abstract Regular (Tree) Model Checking, In: International Journal on Software Tools for Technology Transfer, Vol. 14, No. 2, 2012, DE, p. 167-191, ISSN 1433-2779
 Češka Milan, Fiedor Jan, Gach Marek: A Novel Approach to Modechart Verification of Real-Time systems, In: Lecture Notes in Computer Science, Vol. 2012, No. 6927, DE, p. 559-567, ISSN 0302-9743
 Dudka Kamil, Müller Petr, Peringer Petr, Vojnar Tomáš: Predator: A Verification Tool for Programs with Dynamic Linked Data Structures, In: Lecture Notes in Computer Science, Vol. 2012, No. 7214, DE, p. 544-547, ISSN 0302-9743
 Dudka Kamil, Peringer Petr, Vojnar Tomáš: An Easy to Use Infrastructure for Building Static Analysis Tools, In: Lecture Notes in Computer Science, Vol. 2012, No. 6927, DE, p. 527-534, ISSN 0302-9743
 Fiedor Jan, Hrubá Vendula, Křena Bohuslav, Vojnar Tomáš: DA-BMC: A Tool Chain Combining Dynamic Analysis and Bounded Model Checking, In: Lecture Notes in Computer Science, Vol. 2012, No. 7186, DE, p. 5, ISSN 0302-9743
 Fiedor Jan, Křena Bohuslav, Letko Zdeněk, Vojnar Tomáš: A Uniform Classification of Common Concurrency Errors, In: Lecture Notes in Computer Science, Vol. 2012, No. 6927, DE, p. 519-526, ISSN 0302-9743
 Fiedor Jan, Vojnar Tomáš: ANaConDA: A Framework for Analysing Multi-threaded C/C++ Programs on the Binary Level, In: Lecture Notes in Computer Science, Vol. 2012, No. 7687, DE, p. 35-41, ISSN 0302-9743
 Fiedor Jan, Vojnar Tomáš: Noise-Based Testing and Analysis of Multi-threaded C/C++ Programs on the Binary Level, In: PADTAD '12, New York, US, ACM, 2012, p. 36-46, ISBN 978-1-4503-1456-5
 Habermehl Peter, Holík Lukáš, Rogalewicz Adam, Šimáček Jiří, Vojnar Tomáš: Forest Automata for Verification of Heap Manipulation, In: Formal Methods in System Design, Vol. 2012, No. 41, Berlin, DE, p. 83-106, ISSN 0925-9856
 Hrubá Vendula, Křena Bohuslav, Letko Zdeněk, Ur Shmuel, Vojnar Tomáš: Testing of Concurrent Programs with Genetic Algorithms, In: Lecture Notes in Computer Science, Vol. 2012, No. 7515, DE, p. 152-167, ISSN 0302-9743
 Hrubá Vendula, Křena Bohuslav, Letko Zdeněk, Vojnar Tomáš: Testing of Concurrent Programs Using Genetic Algorithms, FIT-TR-2012-01, Brno, CZ, 2012, p. 31
 Charvát Lukáš, Smrčka Aleš, 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, US, 2012, p. 42-47
 Iosif Radu, Hojjat Hossein, Konečný Filip, Kuncak Viktor, Rummer Philipp: Accelerating Interpolants, In: Lecture Notes in Computer Science, Vol. 2012, No. 7561, DE, p. 187-202, ISSN 0302-9743
 Konečný Filip, Hojjat Hossein, Iosif Radu, Kuncak Viktor, Rummer Philipp, Garnier Florent: A Verification Toolkit for Numerical Transition Systems, In: Lecture Notes in Computer Science, Vol. 2012, No. 7436, DE, p. 247-251, ISSN 0302-9743
 Konečný Filip, Iosif Radu, Bozga Marius: Deciding Conditional Termination, In: Lecture Notes in Computer Science, Vol. 2012, No. 7214, DE, p. 252-266, ISSN 0302-9743
 Křena Bohuslav, Letko Zdeněk, Vojnar Tomáš: Analysis and Testing of Concurrent Programs, Brno, CZ, FIT VUT, 2012, p. 136, ISBN 978-80-214-4464-5
 Křena Bohuslav, Letko Zdeněk, Vojnar Tomáš: Coverage Metrics for Saturation-based and Search-based Testing of Concurrent Software, In: Lecture Notes in Computer Science, Vol. 2012, No. 7186, DE, p. 177-192, ISSN 0302-9743
 Křena Bohuslav, Letko Zdeněk, Vojnar Tomáš: Noise Injection Heuristics for Concurrency Testing, In: Lecture Notes in Computer Science, Vol. 2012, No. 7119, DE, p. 123-131, ISSN 0302-9743
 Lengál Ondřej, Šimáček Jiří, Vojnar Tomáš: VATA: A Library for Efficient Manipulation of Non-Deterministic Tree Automata, In: Lecture Notes in Computer Science, Vol. 2012, No. 7214, DE, p. 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, DE, LAP, 2012, p. 64, ISBN 978-3-659-27069-7
 Novosad Petr, Češka Milan: Unfoldings of Bounded Hybrid Petri Nets, In: Lecture Notes in Computer Science, Vol. 2012, No. 6927, DE, p. 543-550, ISSN 0302-9743
 Šimková Marcela, Lengál Ondřej, Kajan Michal: HAVEN: An Open Framework for FPGA-Accelerated Functional Verification of Hardware, In: Lecture Notes in Computer Science, Vol. 2012, No. 7261, DE, p. 247-253, ISSN 0302-9743
2011Abdulla Parosh A., Chen Yu-Fang, Clemente Lorenzo, Holík Lukáš, Hong Chih-Duo, Mayr Richard, Vojnar Tomáš: Advanced Ramsey-based Büchi Automata Inclusion Testing, FIT-TR-2011-03, Brno, CZ, FIT VUT, 2011, p. 45
 Abdulla Parosh A., Chen Yu-Fang, Clemente Lorenzo, Holík Lukáš, Hong Chih-Duo, Mayr Richard, Vojnar Tomáš: Advanced Ramsey-based Büchi Automata Inclusion Testing, In: Lecture Notes in Computer Science, Vol. 2011, No. 6901, DE, p. 187-202, ISSN 0302-9743
 Bouajjani Ahmed, Bozga Marius, Habermehl Peter, Iosif Radu, Moro Pierre, Vojnar Tomáš: Programs with Lists are Counter Automata, In: Formal Methods in System Design, Vol. 38, No. 2, 2011, Berlin, DE, p. 158-192, ISSN 0925-9856
 Češka Milan, Fiedor Jan, 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, ES, IUCTC, 2011, p. 338-339, ISBN 978-84-693-9560-8
 Dudka Kamil, Peringer Petr, 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, ES, IUCTC, 2011, p. 328-329, ISBN 978-84-693-9560-8
 Dudka Kamil, Peringer Petr, Vojnar Tomáš: Predator: A Practical Tool for Checking Manipulation of Dynamic Data Structures Using Separation Logic, In: Lecture Notes in Computer Science, Vol. 2011, No. 6806, DE, p. 372-378, ISSN 0302-9743
 Dudka Kamil, Peringer Petr, Vojnar Tomáš: Predator: A Practical Tool for Checking Manipulation of Dynamic Data Structures Using Separation Logic, FIT-TR-2011-02, Brno, CZ, FIT VUT, 2011, p. 23
 Fiedor Jan, Hrubá Vendula, Křena Bohuslav, Vojnar Tomáš: DA-BMC: A Tool Chain Combining Dynamic Analysis and Bounded Model Checking, FIT-TR-2011-06, Brno, CZ, FIT VUT, 2011, p. 9
 Fiedor Jan, Křena Bohuslav, Letko Zdeněk, 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, ES, IUCTC, 2011, p. 326-327, ISBN 978-84-693-9560-8
 Habermehl Peter, Holík Lukáš, Rogalewicz Adam, Šimáček Jiří, Vojnar Tomáš: Forest Automata for Verification of Heap Manipulation, In: Lecture Notes in Computer Science, Vol. 2011, No. 6806, DE, p. 424-440, ISSN 0302-9743
 Habermehl Peter, Holík Lukáš, Rogalewicz Adam, Šimáček Jiří, Vojnar Tomáš: Forest Automata for Verification of Heap Manipulation, FIT-TR-2011-01, Brno, CZ, FIT VUT, 2011, p. 30
 Holík Lukáš, Lengál Ondřej, Šimáček Jiří, Vojnar Tomáš: Efficient Inclusion Checking on Explicit and Semi-Symbolic Tree Automata, In: Lecture Notes in Computer Science, Vol. 2011, No. 6996, DE, p. 243-258, ISSN 0302-9743
 Holík Lukáš, Lengál Ondřej, Šimáček Jiří, Vojnar Tomáš: Efficient Inclusion Checking on Explicit and Semi-Symbolic Tree Automata, FIT-TR-2011-04, Brno, CZ, FIT VUT, 2011, p. 22
 Holík Lukáš: Simulations and Antichains for Efficient Handling of Finite Automata, Brno, CZ, UITS FIT VUT, 2011, p. 128
 Šimková Marcela, Lengál Ondřej, Kajan Michal: HAVEN: An Open Framework for FPGA-Accelerated Functional Verification of Hardware, FIT-TR-2011-05, Brno, CZ, FIT VUT, 2011, p. 16
2010Abdulla Parosh A., Clemente Lorenzo, Holík Lukáš, Hong Chih-Duo, Chen Yu-Fang, Mayr Richard, Vojnar Tomáš: Simulation Subsumption in Ramsey-based Büchi Automata Universality and Inclusion Testing, FIT-TR-2010-02, Brno, CZ, FIT VUT, 2010, p. 30
 Abdulla Parosh A., Clemente Lorenzo, Holík Lukáš, Hong Chih-Duo, Chen Yu-Fang, Mayr Richard, Vojnar Tomáš: Simulation Subsumption in Ramsey-Based Büchi Automata Universality and Inclusion Testing, In: Computer Aided Verification, Berlín, DE, Springer, 2010, p. 132-147, ISBN 978-3-642-14294-9
 Abdulla Parosh A., Holík Lukáš, Chen Yu-Fang, Mayr Richard, 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, DE, Springer, 2010, p. 158-174, ISBN 978-3-642-12001-5
 Bozga Marius, Iosif Radu, Konečný Filip: Fast Acceleration of Ultimately Periodic Relations, In: Computer Aided Verification, Berlin, DE, Springer, 2010, p. 227-242, ISBN 978-3-642-14294-9
 Fiedor Jan, Křena Bohuslav, Letko Zdeněk, Vojnar Tomáš: A Uniform Classification of Common Concurrency Errors, FIT-TR-2010-03, Brno, CZ, 2010, p. 24
 Holík Lukáš, Vojnar Tomáš: Simulations and Aintichains for Efficient Handling of Tree Automata, Brno, CZ, FIT VUT, 2010, p. 150, ISBN 978-80-214-4217-7
 Křena Bohuslav, Letko Zdeněk, Ur Shmuel, Vojnar Tomáš: A Platform for Search-Based Testing of Concurrent Software, In: PADTAD '10, Trento, IT, ACM, 2010, p. 11, ISBN 978-1-60558-823-0
 Křena Bohuslav, Letko Zdeněk, Vojnar Tomáš, Ur Shmuel: A Platform for Search-Based Testing of Concurrent Software, 6th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science, Brno, CZ, MUNI, 2010, p. 1, ISBN 978-80-87342-10-7
 Letko Zdeněk: Sophisticated Testing of Concurrent Programs, In: SSBSE '10, Benevento, IT, IEEE, 2010, p. 36-40, ISBN 978-0-7695-4195-2
 Smrčka Aleš, Vojnar Tomáš: Verification of Asynchronous and Parametrized Hardware Designs, Brno, CZ, FIT VUT, 2010, p. 115, ISBN 978-80-214-4214-6
 Smrčka Aleš: Verification of Asynchronous and Parametrized Hardware Designs, Brno, CZ, UITS FIT VUT, 2010, p. 124
 Smrčka Aleš: Verification of Asynchronous and Parametrized Hardware Designs, In: Information Sciences and Technologies Bulletin of the ACM Slovakia, Vol. 2, No. 2, 2010, Bratislava, SK, p. 60-69, ISSN 1338-1237

Your IPv4 address: 107.20.129.212
Switch to IPv6 connection

DNSSEC [dnssec]