Designing verification conditions for software

Abstract

Software verification technology has the potential to improve the quality of software. The basic technique is to generate verification conditions for a given program and to discharge these proof obligations using a theorem prover. Encoding the verification conditions is a delicate process, not just because it must capture the intended programming semantics, but also because it must yield formulas that a theorem prover can process effectively. In this talk, I will discuss the process of generating verification conditions in the program verifier for the object-oriented language Spec#. I will highlight design decisions we have made in modeling programs and targeting SMT solvers, lessons we have learned, and challenges that remain ahead. © Springer-Verlag Berlin Heidelberg 2007.