AIDE

The fundamental challenge of software engineering is that of the complexity of the software being developed. Essentially, the complexity grows faster than what humans can manage when not aided by automated development tools. At the same time, software systems are used in many safety-critical applications (such as various control systems) whose failures can lead to huge financial losses and potentially also endangered human lives. Moreover, not only that software defects can themselves cause failures, they can also be abused for targeted attacks—e.g., in recent years, 70 % of security issues in the Chrome browser as well as in Microsoft products were based on abusing various memory-safety errors such as out-of-bound accesses or use-after-free errors (which belong among the below-mentioned concrete targets of this project).

The overall aim of this project is hence to propose new techniques for automated analysis and verification of advanced software that uses either low-level programming, new high-level constructs, or both. To obtain such methods, we intend to build primarily on our long-term experience with various logic-based approaches (though, if suitable, we may use other approaches too). To facilitate the considered methods, we will also develop or significantly improve decision procedures for various logics suitable for our purposes. Accordingly, we discuss below in more detail the state of the art in analysis and verification of low-level and high-level software (with stress on memory safety in the former case), the verification techniques we intend to improve on, and the decision procedures underlying these techniques.

Related publications