Title: A machine-checked soundness proof for an efficient verification condition generator: technical report
Authors: Vogels, Frédéric
Jacobs, Bart
Piessens, Frank
Issue Date: Apr-2010
Publisher: Department of Computer Science, K.U.Leuven
Series Title: CW Reports vol:CW568
Abstract: 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-the-art 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 paper "A machine-checked soundness proof for an efficient verification condition generator" by the same authors describes a fully formal, machine-checked proof of the soundness of such an efficient VCgen algorithm. This technical report elaborates further on the subject by fully detailing all definitions, theorems and proofs.
Publication status: published
KU Leuven publication type: IR
Appears in Collections:Informatics Section

Files in This Item:
File Description Status SizeFormat
CW568.pdfDocument Published 1277KbAdobe PDFView/Open


All items in Lirias are protected by copyright, with all rights reserved.