SNAPPY

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.

Related publications