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, P., A., Haziza, F., Holík, L., Jonsson, B., Rezine, A.: 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, P., A., Haziza, F., Holík, L.: 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, K., Müller, P., Peringer, P., Vojnar, T.: 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, K., Peringer, P., Vojnar, T.: 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, K., Peringer, P., Vojnar, T.: Byte-Precise Verification of Low-Level List Manipulation, FIT-TR-2012-04, Brno, CZ, FIT VUT, 2013, p. 48
 Holík, L., Lengál, O., Rogalewicz, A., Šimáček, J., Vojnar, T.: Fully Automated Shape Analysis Based on Forest Automata, In: Proceedings of CAV'13, Heidelberg, DE, Springer, 2013, p. 1-16
 Charvát, L., Smrčka, A., Vojnar, T.: 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, R., Rogalewicz, A., Šimáček, J.: The Tree Width of Separation Logic with Recursive Definitions, In: Proceedings of CADE-24, Berlin, DE, 2013, p. 1-18, ISSN 0302-9743
 Iosif, R., Rogalewicz, A., Šimáček, J.: The Tree Width of Separation Logic with Recursive Definitions, arXiv:1301.5139, US, 2013, p. 31
 Křena, B., Vojnar, T.: 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, A., Habermehl, P., Rogalewicz, A., Vojnar, T.: 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, M., Fiedor, J., Gach, M.: 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, K., Müller, P., Peringer, P., Vojnar, T.: 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, K., Peringer, P., Vojnar, T.: 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, J., Hrubá, V., Křena, B., Vojnar, T.: 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, J., Křena, B., Letko, Z., Vojnar, T.: 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, J., Vojnar, T.: 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, J., Vojnar, T.: 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, P., Holík, L., Rogalewicz, A., Šimáček, J., Vojnar, T.: 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á, V., Křena, B., Letko, Z., Ur, S., Vojnar, T.: 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á, V., Křena, B., Letko, Z., Vojnar, T.: Testing of Concurrent Programs Using Genetic Algorithms, FIT-TR-2012-01, Brno, CZ, 2012, p. 31
 Charvát, L., Smrčka, A., Vojnar, T.: 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, R., Hojjat, H., Konečný, F., Kuncak, V., Rummer, P.: Accelerating Interpolants, In: Lecture Notes in Computer Science, Vol. 2012, No. 7561, DE, p. 187-202, ISSN 0302-9743
 Konečný, F., Hojjat, H., Iosif, R., Kuncak, V., Rummer, P., Garnier, F.: 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ý, F., Iosif, R., Bozga, M.: Deciding Conditional Termination, In: Lecture Notes in Computer Science, Vol. 2012, No. 7214, DE, p. 252-266, ISSN 0302-9743
 Křena, B., Letko, Z., Vojnar, T.: Analysis and Testing of Concurrent Programs, Brno, CZ, FIT VUT, 2012, p. 136, ISBN 978-80-214-4464-5
 Křena, B., Letko, Z., Vojnar, T.: 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, B., Letko, Z., Vojnar, T.: 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, O., Šimáček, J., Vojnar, T.: 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, O.: 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, P., Češka, M.: Unfoldings of Bounded Hybrid Petri Nets, In: Lecture Notes in Computer Science, Vol. 2012, No. 6927, DE, p. 543-550, ISSN 0302-9743
 Šimková, M., Lengál, O., Kajan, M.: 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, P., A., Chen, Y., Clemente, L., Holík, L., Hong, C., Mayr, R., Vojnar, T.: Advanced Ramsey-based Büchi Automata Inclusion Testing, FIT-TR-2011-03, Brno, CZ, FIT VUT, 2011, p. 45
 Abdulla, P., A., Chen, Y., Clemente, L., Holík, L., Hong, C., Mayr, R., Vojnar, T.: 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, A., Bozga, M., Habermehl, P., Iosif, R., Moro, P., Vojnar, T.: 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, M., Fiedor, J., Gach, M.: 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, K., Peringer, P., Vojnar, T.: 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, K., Peringer, P., Vojnar, T.: 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, K., Peringer, P., Vojnar, T.: 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, J., Hrubá, V., Křena, B., Vojnar, T.: DA-BMC: A Tool Chain Combining Dynamic Analysis and Bounded Model Checking, FIT-TR-2011-06, Brno, CZ, FIT VUT, 2011, p. 9
 Fiedor, J., Křena, B., Letko, Z., Vojnar, T.: 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, P., Holík, L., Rogalewicz, A., Šimáček, J., Vojnar, T.: 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, P., Holík, L., Rogalewicz, A., Šimáček, J., Vojnar, T.: Forest Automata for Verification of Heap Manipulation, FIT-TR-2011-01, Brno, CZ, FIT VUT, 2011, p. 30
 Holík, L., Lengál, O., Šimáček, J., Vojnar, T.: 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, L., Lengál, O., Šimáček, J., Vojnar, T.: Efficient Inclusion Checking on Explicit and Semi-Symbolic Tree Automata, FIT-TR-2011-04, Brno, CZ, FIT VUT, 2011, p. 22
 Holík, L.: Simulations and Antichains for Efficient Handling of Finite Automata, Brno, CZ, UITS FIT VUT, 2011, p. 128
 Šimková, M., Lengál, O., Kajan, M.: HAVEN: An Open Framework for FPGA-Accelerated Functional Verification of Hardware, FIT-TR-2011-05, Brno, CZ, FIT VUT, 2011, p. 16
2010Abdulla, P., A., Clemente, L., Holík, L., Hong, C., Chen, Y., Mayr, R., Vojnar, T.: Simulation Subsumption in Ramsey-based Büchi Automata Universality and Inclusion Testing, FIT-TR-2010-02, Brno, CZ, FIT VUT, 2010, p. 30
 Abdulla, P., A., Clemente, L., Holík, L., Hong, C., Chen, Y., Mayr, R., Vojnar, T.: 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, P., A., Holík, L., Chen, Y., Mayr, R., Vojnar, T.: 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, M., Iosif, R., Konečný, F.: Fast Acceleration of Ultimately Periodic Relations, In: Computer Aided Verification, Berlin, DE, Springer, 2010, p. 227-242, ISBN 978-3-642-14294-9
 Fiedor, J., Křena, B., Letko, Z., Vojnar, T.: A Uniform Classification of Common Concurrency Errors, FIT-TR-2010-03, Brno, CZ, 2010, p. 24
 Holík, L., Vojnar, T.: Simulations and Aintichains for Efficient Handling of Tree Automata, Brno, CZ, FIT VUT, 2010, p. 150, ISBN 978-80-214-4217-7
 Křena, B., Letko, Z., Ur, S., Vojnar, T.: 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, B., Letko, Z., Vojnar, T., Ur, S.: 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, Z.: Sophisticated Testing of Concurrent Programs, In: SSBSE '10, Benevento, IT, IEEE, 2010, p. 36-40, ISBN 978-0-7695-4195-2
 Smrčka, A., Vojnar, T.: Verification of Asynchronous and Parametrized Hardware Designs, Brno, CZ, FIT VUT, 2010, p. 115, ISBN 978-80-214-4214-6
 Smrčka, A.: Verification of Asynchronous and Parametrized Hardware Designs, Brno, CZ, UITS FIT VUT, 2010, p. 124
 Smrčka, A.: 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]