Verified Functional Programming of an Abstract Interpreter

TL;DR

This paper introduces a fully verified abstract interpreter implemented in F*, demonstrating correctness and reducing proof effort through refinement types and SMT solving, with most code and proofs presented in the paper.

Contribution

It presents a fully verified abstract interpreter in F* that simplifies proof development using refinement types and SMT, making formal verification more accessible.

Findings

Significant reduction in proof effort compared to previous verified interpreters

Implementation and proofs are written in a functional style within the paper

Demonstrates the practical use of F* for verified software development

Abstract

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.