Skip to Main content Skip to Navigation
Conference papers

Verified Functional Programming of an Abstract Interpreter

Lucas Franceschino 1 Jean-Pierre Talpin 2 David Pichardie 3 
1 TEA - Tim, Events and Architectures
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
3 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : Interpreters are complex pieces of software: even if the abstract interpretation theory and companion algorithms are well understood, their implementations are subject to bugs, that might question the soundness of their computations. While some formally verified abstract interpreters have been written in the past, writing and understanding them requires expertise in the use of proof assistants, and requires a non-trivial amount of interactive proofs. This paper presents a formally verified abstract interpreter fully programmed and proved correct in the F* verified programming environment. Thanks to F* refinement types and SMT prover capabilities we demonstrate a substantial saving in proof effort compared to previous works based on interactive proof assistants. Almost all the code of our implementation, proofs included, written in a functional style, are presented directly in the paper.
Document type :
Conference papers
Complete list of metadata

https://hal.inria.fr/hal-03342997
Contributor : Jean-Pierre Talpin Connect in order to contact the contributor
Submitted on : Monday, September 13, 2021 - 5:11:15 PM
Last modification on : Saturday, August 6, 2022 - 3:33:02 AM

File

sas21.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-03342997, version 1

Citation

Lucas Franceschino, Jean-Pierre Talpin, David Pichardie. Verified Functional Programming of an Abstract Interpreter. SAS 2021 - 28th Static Analysis Symposium, Oct 2021, Chicago, United States. pp.1-20. ⟨hal-03342997⟩

Share

Metrics

Record views

50

Files downloads

83