Studying Verification Conditions for Imperative Programs

Cláudio Belo Lourenço, Si-Mohamed Lamraoui, Shin Nakajima, Jorge Sousa Pinto


Program verification tools use verification condition generators to produce logical formulas whose validity implies that the program is correct with respect to its specification. Different tools produce different conditions, and the underlying algorithms have not been properly exposed or explored so far. In this paper we consider a simple imperative programming language, extended with assume and assert statements, to present different ways of generating verification conditions. We study the approaches with  experimental results originated by verification conditions generated from the intermediate representation of LLVM.

Full Text:




Hosted By Universitätsbibliothek TU Berlin.