Automated software verification and bug hunting are a hot topic in both industry and academia. Indeed, they can save a lot of money and, in case of safety-critical software, even human lives. This project aims at new automated methods of static formal verification (based on approaches like symbolic verification or automated abstraction) as well as extrapolating dynamic analysis and advanced testing of programs that use several classes of advanced programming constructions. In particular, the project concentrates on pointer programs, concurrent programs (including cloud programs), and container programs. While these areas are to some degree independent, there is also a lot of overlap among them: On the one hand, one needs to consider various combinations of the mentioned constructions (e.g., concurrent pointer programs). On the other hand, one needs to solve similar problems for all of them. An important example of the latter considered in the project is dealing with open programs, i.e., program fragments that the programmers need to verify despite their environment is unknown.
The goal of the project is to develop new methods of automated static formal verification (based on approaches like symbolic verification or abstraction) as well as extrapolating dynamic analysis and testing for advanced programs using pointers, concurrency (including the cloud), and/or containers.
Project id: 17-12465S