Title: A machine checked soundness proof for an intermediate verification language: extended version
Authors: Vogels, Frédéric
Jacobs, Bart
Piessens, Frank
Issue Date: Oct-2008
Publisher: Department of Computer Science, K.U.Leuven
Series Title: CW Reports vol:CW526
Abstract: Machine-checked proofs of properties of programming languages have gained in importance significantly over the past few years. This paper contributes to this trend by proposing an approach for doing machine-checked soundness proofs for verification condition (VC) generators. Our approach embraces the multi-phase VC generation common in modern program verifiers. Such verifiers split the generation of VCs in two (or even more) phases, using an intermediate verification language as the bridge between the programming language and logic. In our approach, we define a formal operational semantics of the intermediate verification language, and we prove the soundness of two translations separately: (1) the translation of the intermediate verification language to VCs, and (2) the translation of the source programming language to the intermediate language. This paper presents a fully machine checked proof of step (1) for a prototypical intermediate verification language, and then illustrates step (2) for a very small object oriented programming language.
Publication status: published
KU Leuven publication type: IR
Appears in Collections:Informatics Section

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


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