A machine checked soundness proof for an intermediate verification language

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 very small object oriented programming language. © Springer-Verlag Berlin Heidelberg 2009.