Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

Continuation Passing as an Abstract Syntax for Deductive Verification

Andrei Paskevich 1
1 TOCCATA - Formally Verified Programs, Certified Tools and Numerical Computations
Inria Saclay - Ile de France, LMF - Laboratoire Méthodes Formelles
Abstract : Continuation-passing style allows us to devise an extremely economical abstract syntax for a generic algorithmic language. This syntax is flexible enough to naturally express conditionals, loops, (higher-order) function calls, and exception handling. It is type-agnostic and state-agnostic, which means that we can combine it with a wide range of type and effect systems. We argue that this syntax is also well suited for the purposes of deductive verification. Indeed, we show how it can be augmented in a natural way with specification annotations, ghost code, and side-effect discipline. We define the rules of verification condition generation for this syntax, and we show that the resulting formulas are nearly identical to what traditional approaches, like the weakest precondition calculus, produce for the equivalent algorithmic constructions. To sum up, we propose a minimalistic yet versatile abstract syntax for annotated programs for which we can compute verification conditions without sacrificing their size, legibility, and amenability to automated proof, compared to more traditional methods. We believe that it makes it an excellent candidate for internal code representation in program verification tools.
Document type :
Preprints, Working Papers, ...
Complete list of metadata

https://hal.inria.fr/hal-03115120
Contributor : Andrei Paskevich Connect in order to contact the contributor
Submitted on : Tuesday, January 19, 2021 - 1:59:08 PM
Last modification on : Friday, January 21, 2022 - 3:11:27 AM
Long-term archiving on: : Tuesday, April 20, 2021 - 7:31:24 PM

File

leiden.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-03115120, version 1

Citation

Andrei Paskevich. Continuation Passing as an Abstract Syntax for Deductive Verification. 2021. ⟨hal-03115120⟩

Share

Metrics

Les métriques sont temporairement indisponibles