This project targets the area of automated verification of computer systems, which currently attracts a lot of attention both in academia as well as industry. The reasons are clear: The complexity of computer systems is constantly growing, and it is more and more difficult to ensure their correct functionality. At the same time, many fully automated computer systems are used in increasingly critical applications (such as control of industrial plants, cars, planes, space devices, etc.). Moreover, expectations of users to be provided with reliable products are growing even for common everyday applications (e.g., office software or various home electronics that is nowadays usually computer-controlled).

The high-level goal of this project is to significantly improve the generality, automation, and efficiency of symbolic formal analysis and verification of infinite-state programs and hence to address the challenges described in the preceding section. Our approach is based on the conviction that these challenges require a novel development and combination of techniques from a wide range of different areas including model checking, abstract interpretation, automata theory, and applied logic. Our research groups have a strong background in these areas, and we believe that by joining our forces and by also cooperating with researchers from our wide international collaboration networks, we will be able to make a considerable push in the state of the art.

Pavel Parízek, Ondřej Lhoták:
Fast Detection of Concurrency Errors by State Space Traversal with Randomization and Early Backtracking, in International Journal on Software Tools for Technology Transfer 2018(0), 
DOI: 10.1007/s10009-018-0484-7, 2018
Pavel Jančík, Jan Kofroň:
On partial state matching, in Formal Aspects of Computing 29(5),  pp. 777-803
DOI: 10.1007/s00165-016-0413-z, 2017
Pavel Jančík, Jan Kofroň:
Dead Variable Analysis for Multi-threaded Heap Manipulating Programs, in Proceedings of the 31st Annual ACM Symposium on Applied Computing,  ISBN: 978-1-4503-3739-7, pp. 1620–1627
DOI: 10.1145/2851613.2851826, 2016
Pavel Parízek:
Hybrid Partial Order Reduction with Under-Approximate Dynamic Points-to and Determinacy Information, in 2016 Formal Methods in Computer-Aided Design, FMCAD 2016, Mountain View, CA, USA, October 3-6, 2016,  pp. 141–148
DOI: 10.1109/FMCAD.2016.7886672, 2016
Pavel Parízek:
Fast Error Detection with Hybrid Analyses of Future Accesses, in Proceedings of the 31st Annual ACM Symposium on Applied Computing, Pisa, Italy, April 4-8, 2016,  pp. 1251–1254
DOI: 10.1145/2851613.2851935, 2016
Pavel Jančík, Leonardo Alt, Grigory Fedyukovich, Antti E. J. Hyvärinen, Jan Kofroň, Natasha Sharygina:
PVAIR: Partial Variable Assignment InterpolatoR, in Proceedings of FASE 2016,  ISBN: 978-3-662-49665-7, pp. 419-434
DOI: 10.1007/978-3-662-49665-7_25, 2016
Jakub Daniel, Alessandro Cimatti, Alberto Griggio, Stefano Tonetta, Sergio Mover:
Infinite-State Liveness-to-Safety via Implicit Abstraction and Well-Founded Relations, in CAV'16,  ISBN: 978-3-319-41528-4, pp. 271-291
DOI: 10.1007/978-3-319-41528-4_15, 2016
Project data
Duration: 2014-2016
ID: 14-11384S