Student Projects in Automated Reasoning about Programs

Contact: Laura Kovács

The logically deep parts of the code are characterized by loops or recursions. For these parts, formal program verification is an appropriate tool. One of its biggest challenges is the automated discovery of auxiliary program assertions, leading to the discovery of safety and liveness properties of programs.

The increasing power of automated theorem proving and computer algebra have opened new perspectives for computer aided program verification, in particular for the automatic generation of invariant assertions and ranking functions in order to reason about loops and recursion. Especially promising breakthroughs are the assertion generation techniques by first-order theorem proving, satisfiability modulo theory (SMT) reasoning, and symbolic computation. These techniques can efficiently be used in conjunction with model checking, interpolation, static analysis, abstract interpretation, symbolic execution, or game-theoretic investigations.

We offer student projects (semester, master, PhD) dealing with the design of efficient methods for automated reasoning and generation of program assertions.

Project topics include, but are not limited to:

• design of theory and algorithms of:
  • automating deductive verification (using e.g. Hoare logic, weakest preconditions);
  • inferring program assertions, such as loop invariants and ranking functions;
  • statically analyzing deterministic and/or probabilistic programs;
  • interpolation/abduction-based verification techniques in the combination of the first-order theories of data structures; 
  • first-order theorem proving in support of software verification;
  • relational verification of security and privacy properties; 
  • game-theoretic analysis of system requirements; 

• case studies/experimental evaluations using:
  • available methods for the generation of program assertions;
  • automated theorem provers and SMT solvers.

Improvements and extensions on the existing algorithms for software verification are highly welcomed.