Core Concepts
The core message of this paper is to present a novel methodology for automatically generating formal proofs that validate the soundness of front-end translations from a source language (e.g. Viper) to an intermediate verification language (e.g. Boogie) used in practical program verification tools.
Abstract
The paper presents a methodology for formally validating the soundness of front-end translations used in practical program verification tools. The key points are:
Existing work on ensuring front-end soundness is based on idealized implementations, leaving a large gap to the actual translations used in practice. The authors bridge this gap by developing an approach to formally validate the front-end soundness of translations used in existing, practical verifier implementations.
The authors develop a general methodology for the automatic validation of front-end translations based on forward simulation proofs. This methodology is presented for the translation from Viper to Boogie, which exhibits key challenges such as the semantic gap between the languages, diverse translations, and non-locality of translation checks.
The authors instrument the existing Viper-to-Boogie implementation to automatically generate Isabelle proofs justifying the soundness of the translation. These generated proofs can be checked independently in Isabelle, ensuring front-end soundness of the Viper verifier.
The evaluation demonstrates the effectiveness of the approach by generating and checking proofs fully automatically for a diverse set of Viper programs.
As part of the work, the authors provide the first approach to formally deal with a restricted version of Boogie's polymorphic maps.