Software Verification in Practice

Software verification entails the algorithmic analysis of programs to mathematically prove properties of their executions - to prove that given certain assumptions, the code is correct and bug-free. It has found extensive application in embedded, cyber-physical, and safety-critical systems. Among others, it allows verifying array bounds (for absence of buffer overflows), pointer safety, exceptions and user-specified assertions. This project will investigate software engineering aspects of applying verification in practice.