Automated Program Reasoning

The Automated Program Reasoning - APRe group focuses on the design and development of new theories, technologies, and tools for automating program analysis, with a particular focus on generating and proving program properties that can prevent programmers introducing errors while making changes in their code. The APRe research therefore focuses, among others, on algebra-based program analysis, loop invariant synthesis, proving loop termination, probablistic programming, SMT solving, first-order theorem proving, inductive reasoning, and security analysis.