Sciweavers

Share
SAC
2010
ACM

A machine-checked soundness proof for an efficient verification condition generator

9 years 1 months ago
A machine-checked soundness proof for an efficient verification condition generator
Verification conditions (VCs) are logical formulae whose validity implies the correctness of a program with respect to a specification. The technique of checking software properties by specifying them in a program logic, then generating VCs, and finally feeding these VCs to a theorem prover, is several decades old. It is the underlying technology for state-of-theart program verifiers such as the Spec programming system, or ESC/Java. The classic way of computing VCs is by means of Dijkstra's weakest precondition calculus. However, modern verification condition generators (VCgens), including Spec and ESC/Java's VCgens, are based on an optimized version of this algorithm, that avoids an exponential growth of the VCs in the length of the program to be verified. For this optimized VCgen algorithm, only informal soundness arguments are available. The main contribution of this paper is a fully formal, machine-checked proof of the soundness of such an efficient VCgen algorithm. Cate...
Frédéric Vogels, Bart Jacobs 0002, F
Added 14 Feb 2011
Updated 14 Feb 2011
Type Journal
Year 2010
Where SAC
Authors Frédéric Vogels, Bart Jacobs 0002, Frank Piessens
Comments (0)
books