Statická a dynamická verifikace programů s pokročilými rysy paralelismu a neomezenosti

English title

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

Type

grant

Keywords

automated verification of programs; static and dynamic analysis; formal verification; model checking; concurrency; infinite-state programs; dynamic data structures

Abstract

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.

Team members

Vojnar Tomáš, prof. Ing., Ph.D. (UITS FIT VUT) , research leader
Češka Milan, prof. RNDr., CSc. (UITS FIT VUT) , team leader
Křena Bohuslav, Ing., Ph.D. (UITS FIT VUT) , team leader
Peringer Petr, Dr. Ing. (UITS FIT VUT) , team leader
Rogalewicz Adam, doc. Mgr., Ph.D. (UITS FIT VUT) , team leader
Smrčka Aleš, Ing., Ph.D. (UITS FIT VUT) , team leader
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)

Publications

2015

FIEDOR 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, vol. 25, no. 3, 2015, pp. 272-309. ISSN 1099-1689. Detail

2013

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. Detail
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. Lecture Notes in Computer Science, vol. 8111. Berlin Heidelberg: Springer Verlag, 2013, pp. 460-468. ISBN 978-3-642-53855-1. Detail
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. Lecture Notes in Computer Science, vol. 7795. Berlin Heidelberg: Springer Verlag, 2013, pp. 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, vol. 5, no. 3, 2013, pp. 1-8. ISSN 1338-1237. Detail
IOSIF Radu and ROGALEWICZ Adam. Automata-Based Termination Proofs. Computing and Informatics, vol. 2013, no. 4, pp. 739-775. ISSN 1335-9150. Detail
KŘENA Bohuslav and VOJNAR Tomáš. Automated formal analysis and verification: an overview. International Journal of General Systems, vol. 2013, no. 42, pp. 335-365. ISSN 0308-1079. Detail
DUDKA Kamil, PERINGER Petr and VOJNAR Tomáš. Byte-Precise Verification of Low-Level List Manipulation. In: 20th Static Analysis Symposium. Lecture Notes in Computer Science Volume 7935, vol. 20. Berlin: Springer Verlag, 2013, pp. 215-237. ISBN 978-3-642-38855-2. ISSN 0302-9743. Detail
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. Detail
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. Detail
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. Detail
ABDULLA Parosh A., CEDERBERG Jonathan and VOJNAR Tomáš. Monotonic Abstraction for Programs with Multiply-Linked Structures. International Journal of Foundations of Computer Science, vol. 24, no. 2, 2013, pp. 187-210. ISSN 0129-0541. Detail
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. Lecture Notes in Computer Science Volume 7795, vol. 2013. Berlin: Springer Verlag, 2013, pp. 627-629. ISBN 978-3-642-36742-7. ISSN 0302-9743. Detail
IOSIF Radu, ROGALEWICZ Adam and ŠIMÁČEK Jiří. The Tree Width of Separation Logic with Recursive Definitions. In: Automated Deduction - CADE-24. Lecture Notes in Artificial Intelligence, vol. 2013. Berlin: Springer Verlag, 2013, pp. 21-38. ISBN 978-3-642-38573-5. ISSN 0302-9743. Detail
IOSIF Radu, ROGALEWICZ Adam and Š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 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. Detail
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. Detail

2012

ČEŠKA Milan, FIEDOR Jan and GACH Marek. A Novel Approach to Modechart Verification of Real-Time systems. Lecture Notes in Computer Science, vol. 2012, no. 6927, pp. 559-567. ISSN 0302-9743. Detail
FIEDOR Jan, KŘENA Bohuslav, LETKO Zdeněk and VOJNAR Tomáš. A Uniform Classification of Common Concurrency Errors. Lecture Notes in Computer Science, vol. 2012, no. 6927, pp. 519-526. ISSN 0302-9743. Detail
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, vol. 2012, no. 7436, pp. 247-251. ISSN 0302-9743. Detail
BOUAJJANI Ahmed, HABERMEHL Peter, ROGALEWICZ Adam and VOJNAR Tomáš. Abstract Regular (Tree) Model Checking. International Journal on Software Tools for Technology Transfer, vol. 14, no. 2, 2012, pp. 167-191. ISSN 1433-2779. Detail
IOSIF Radu, HOJJAT Hossein, KONEČNÝ Filip, KUNCAK Viktor and RUMMER Philipp. Accelerating Interpolants. Lecture Notes in Computer Science, vol. 2012, no. 7561, pp. 187-202. ISSN 0302-9743. Detail
DUDKA Kamil, PERINGER Petr and VOJNAR Tomáš. An Easy to Use Infrastructure for Building Static Analysis Tools. Lecture Notes in Computer Science, vol. 2012, no. 6927, pp. 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 and VOJNAR Tomáš. ANaConDA: A Framework for Analysing Multi-threaded C/C++ Programs on the Binary Level. Lecture Notes in Computer Science, vol. 2012, no. 7687, pp. 35-41. ISSN 0302-9743. Detail
KŘENA Bohuslav, LETKO Zdeněk and VOJNAR Tomáš. Analysis and Testing of Concurrent Programs. FIT Monograph. Brno: Faculty of Information Technology BUT, 2012. ISBN 978-80-214-4464-5. Detail
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. Detail
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, vol. 2012, no. 7186, pp. 177-192. ISSN 0302-9743. Detail
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, vol. 2012, no. 7186, p. 5. ISSN 0302-9743. Detail
KONEČNÝ Filip, IOSIF Radu and BOZGA Marius. Deciding Conditional Termination. Lecture Notes in Computer Science, vol. 2012, no. 7214, pp. 252-266. ISSN 0302-9743. Detail
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, vol. 2012, no. 41, pp. 83-106. ISSN 0925-9856. Detail
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, vol. 2012, no. 7261, pp. 247-253. ISSN 0302-9743. Detail
KŘENA Bohuslav, LETKO Zdeněk and VOJNAR Tomáš. Noise Injection Heuristics for Concurrency Testing. Lecture Notes in Computer Science, vol. 2012, no. 7119, pp. 123-131. ISSN 0302-9743. Detail
FIEDOR Jan and 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, pp. 36-46. ISBN 978-1-4503-1456-5. Detail
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, vol. 2012, no. 7214, pp. 544-547. ISSN 0302-9743. Detail
DUDKA Vendula, KŘENA Bohuslav, LETKO Zdeněk and 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 and VOJNAR Tomáš. Testing of Concurrent Programs with Genetic Algorithms. Lecture Notes in Computer Science, vol. 2012, no. 7515, pp. 152-167. ISSN 0302-9743. Detail
NOVOSAD Petr and ČEŠKA Milan. Unfoldings of Bounded Hybrid Petri Nets. Lecture Notes in Computer Science, vol. 2012, no. 6927, pp. 543-550. ISSN 0302-9743. Detail
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, vol. 2012, no. 7214, pp. 79-94. ISSN 0302-9743. Detail

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. Detail
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. Detail
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. FIT-TR-2011-03, Brno: Faculty of Information Technology BUT, 2011. Detail
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, vol. 2011, no. 6901, pp. 187-202. ISSN 0302-9743. Detail
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. Detail
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. Detail
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, vol. 2011, no. 6996, pp. 243-258. ISSN 0302-9743. Detail
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. Detail
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, vol. 2011, no. 6806, pp. 424-440. ISSN 0302-9743. Detail
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. Detail
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. Detail
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, vol. 2011, no. 6806, pp. 372-378. ISSN 0302-9743. Detail
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. Detail
BOUAJJANI Ahmed, BOZGA Marius, HABERMEHL Peter, IOSIF Radu, MORO Pierre and VOJNAR Tomáš. Programs with Lists are Counter Automata. Formal Methods in System Design, vol. 38, no. 2, 2011, pp. 158-192. ISSN 0925-9856. Detail

2010

KŘENA Bohuslav, LETKO Zdeněk, UR Shmuel and 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, p. 11. ISBN 978-1-60558-823-0. Detail
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. Detail
FIEDOR Jan, KŘENA Bohuslav, LETKO Zdeněk and VOJNAR Tomáš. A Uniform Classification of Common Concurrency Errors. FIT-TR-2010-03, Brno, 2010. Detail
BOZGA Marius, IOSIF Radu and KONEČNÝ Filip. Fast Acceleration of Ultimately Periodic Relations. In: Computer Aided Verification. Lecture Notes in Computer Science, vol. 6174. Berlin: Springer Verlag, 2010, pp. 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 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. Detail
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. Lecture Notes in Computer Science, vol. 6174. Berlín: Springer Verlag, 2010, pp. 132-147. ISBN 978-3-642-14294-9. Detail
HOLÍK Lukáš and VOJNAR Tomáš. Simulations and Aintichains for Efficient Handling of Tree Automata. FIT Monograph. Brno: Faculty of Information Technology BUT, 2010. ISBN 978-80-214-4217-7. Detail
LETKO Zdeněk. Sophisticated Testing of Concurrent Programs. In: SSBSE '10. Proceedings of 2nd International Symposium on Search Based Software Engineering. Benevento: Institute of Electrical and Electronics Engineers, 2010, pp. 36-40. ISBN 978-0-7695-4195-2. Detail
SMRČKA Aleš and VOJNAR Tomáš. Verification of Asynchronous and Parametrized Hardware Designs. FIT Monograph. Brno: Faculty of Information Technology BUT, 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, vol. 2, no. 2, 2010, pp. 60-69. ISSN 1338-1237. Detail
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. Lecture Notes in Computer Science, vol. 6015. Berlín: Springer Verlag, 2010, pp. 158-174. ISBN 978-3-642-12001-5. Detail

Products

2013

CPAlien: Configurable Program Analysis over Symbolic Memory Graphs, software, 2013
Authors: Müller Petr, Vojnar Tomáš Detail

2012

ANaConDA: A Framework for Analysing Multi-threaded C/C++ Programs on the Binary Level, software, 2012
Authors: Fiedor Jan, Vojnar Tomáš Detail
HAVEN: An Open Framework for FPGA-Accelerated Functional Verification of Hardware, software, 2012
Authors: Zachariášová Marcela, Lengál Ondřej, Kajan Michal Detail
VATA: A Library for Efficient Manipulation of Non-Deterministic Tree Automata, software, 2012
Authors: Lengál Ondřej, Šimáček Jiří, Vojnar Tomáš Detail

2011

A Tool Chain Combining Dynamic Analysis and Bounded Model Checking, software, 2011
Authors: Dudka Vendula, Fiedor Jan, Křena Bohuslav, Vojnar Tomáš Detail

2010

An Easy to Use Infrastructure for Building Static Analysis Tools, software, 2010
Authors: Dudka Kamil, Peringer Petr, Vojnar Tomáš Detail
Forester: A Tool for Verification of Programs with Pointers, software, 2010
Authors: Habermehl Peter, Holík Lukáš, Rogalewicz Adam, Šimáček Jiří, Vojnar Tomáš Detail
Framework for Formal Verification of Clock Domain Crossing, software, 2010
Authors: Smrčka Aleš, Vojnar Tomáš Detail
libSFTA: A Semi-symbolic Nondeterministic Finite Tree Automata Library Prototype, software, 2010
Authors: Holík Lukáš, Lengál Ondřej, Vojnar Tomáš Detail
Predator: A Tool for Checking Manipulation of Dynamic Data Structures Using Separation Logic, software, 2010
Authors: Dudka Kamil, Peringer Petr, Vojnar Tomáš Detail
Replay Tracer & BMC, software, 2010
Authors: Dudka Vendula, Fiedor Jan, Křena Bohuslav, Letko Zdeněk, Vojnar Tomáš Detail
Search-based Testing Environment (SearchBestie), software, 2010
Authors: Letko Zdeněk, Vojnar Tomáš, Křena Bohuslav Detail
Tool for verification of systems described using the Modechart formalism, software, 2010
Authors: Gach Marek, Fiedor Jan, Češka Milan Detail
Tool for verification of systems specified in RT-Logic language, software, 2010
Authors: Fiedor Jan, Gach Marek, Češka Milan Detail