Due to the complexity of current software and the rising requirements on its reliability, traditional testing no longer suffices to assure the needed quality, and automated analysis and verification methods are needed. However, despite a lot of recent progress in this area, the current methods are still lacking in scalability, precision, and/or capabilities of analysing complex properties of advanced code. This is exactly what the project aims to attack, concentrating on several complementary types of program constructions that are particularly problematic for current automated analyses: namely, low-level pointer operations, dealing with arrays and strings, and concurrency. Both static approaches based on abstract interpretation and model checking as well as dynamic analysis based on extrapolation and noise injection will be studied. In the former case, a special attention will be devoted to approaches based on SAT/SMT solving, including improvements of the decision procedures used.
The goal of the project is to significantly improve state-of-the-art techniques of automated analysis and verification to make them more scalable and applicable for handling more complex properties of more complex code with low-level pointer operations, arrays, strings, and/or concurrency.
Using linear algebra in decomposition of Farkas interpolants, in International Journal on Software Tools for Technology Transfer 24(1), pp. 111-125, 2022
Transition Power Abstractions for Deep Counterexample Detection, in Tools and Algorithms for the Construction and Analysis of Systems, pp. 524-542, 2022
ISBN: 978-3-030-99524-9, DOI: 10.1007/978-3-030-99524-9_29
Incremental Verification by SMT-based Summary Repair, in Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design – FMCAD 2020, 2020
ISBN: 978-3-85448-042-6, DOI: 10.34727/2020/isbn.978-3-85448-042-6
Funding body: Czech Science Foundation
Contact: Jan Kofroň