An Efficient VCGen-based Modular Verification of Relational Properties

TL;DR

The paper addresses the challenge of verifying relational properties that relate multiple function calls within modular verification. It presents an optimized verification condition generator (VCGen) for a minimal language with procedures and pointers, extended to support relational properties via relational contracts and modular proofs, formalized and proved sound in Coq. A key contribution is the integration of relational properties as hypotheses and the extension of the VCGen to generate and check both auxiliary and relational verification conditions, ensuring that relational contracts imply the target relational postconditions. The work enables modular verification of relational properties without code transformations, improving practicality for real languages with aliasing, and provides a fully mechanized Coq development including correctness proofs.

Abstract

Deductive verification typically relies on function contracts that specify the behavior of each function for a single function call. Relational properties link several function calls together within a single specification. They can express more advanced properties of a given function, such as non-interference, continuity, or monotonicity, or relate calls to different functions, possibly run in parallel, for instance, to show the equivalence of two implementations. However, relational properties cannot be expressed and verified directly in the traditional setting of modular deductive verification. Recent work proposed a new technique for relational property verification that relies on a verification condition generator to produce logical formulas that must be verified to ensure a given relational property. This paper presents an overview of this approach and proposes important enhancements. We integrate an optimized verification condition generator and extend the underlying theory to show how relational properties can be proved in a modular way, where one relational property can be used to prove another one, like in modular verification of function contracts. Our results have been fully formalized and proved sound in the Coq proof assistant.

Figures (1)

• Figure 1: Recursive command ${c_\mathrm{sum}}$, associated as a body with procedure name ${y_\mathrm{sum}}$, and relational property $\mathcal{R}_1$ between two commands, denoted ${c_\omega^1}$ and ${c_\omega^2}$, involving a call to this procedure.