Room 206 (2nd floor, badged access)
11 avril 2024 - 14h30
Coma: an intermediate verification language with explicit abstraction barriers
par Andrei Paskevich de Univ. Paris-Saclay (LMF) - Inria Saclay (Toccata)
Abstract: Coma is a minimalistic algorithmic language designed for deductive verification. It adopts the continuation-passing style which allows us to express in a natural manner the standard control structures — conditionals, loops, subroutine calls, and exception handling — using only three elementary constructions.
The specification annotations in Coma take the form of assertions mixed with the rest of the program code. A special barrier tag is used to separate, inside a subroutine definition, the interface part of the code, which should be verified at each call, from the implementation part, which is verified only once, for all possible inputs. In comparison with traditional contract-based specification, this offers us an additional degree of freedom, as we can provide separate specification for different execution paths in the code. We can also forgo the barriers entirely for some (or all) of the paths, which effectively inlines the corresponding code during the computation of verification conditions.
Verification conditions for Coma programs are structurally similar to what is generated by the classical weakest-precondition calculus. However, our procedure can also factorize the instances of selected subformulas in the resulting proof obligation, which leads to more compact verification conditions in the style of Flanagan and Saxe.
