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.
Related publications
Fast Detection of Concurrency Errors by State Space Traversal with Randomization and Early Backtracking, in International Journal on Software Tools for Technology Transfer 21(4), pp. 365-400, 2019
DOI: 10.1007/s10009-018-0484-7
On partial state matching, in Formal Aspects of Computing 29(5), pp. 777-803, 2017
DOI: 10.1007/s00165-016-0413-z
Dead Variable Analysis for Multi-threaded Heap Manipulating Programs, in Proceedings of the 31st Annual ACM Symposium on Applied Computing, pp. 1620–1627, 2016
ISBN: 978-1-4503-3739-7, DOI: 10.1145/2851613.2851826
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, 2016
DOI: 10.1145/2851613.2851935
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, 2016
DOI: 10.1109/FMCAD.2016.7886672
Infinite-State Liveness-to-Safety via Implicit Abstraction and Well-Founded Relations, in CAV'16, pp. 271-291, 2016
ISBN: 978-3-319-41528-4, DOI: 10.1007/978-3-319-41528-4_15
PVAIR: Partial Variable Assignment InterpolatoR, in Proceedings of FASE 2016, pp. 419-434, 2016
ISBN: 978-3-662-49665-7, DOI: 10.1007/978-3-662-49665-7_25