We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs.PL

Change to browse by:

cs

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Programming Languages

Title: Verified Functional Programming of an Abstract Interpreter

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.
Comments: To be published in SAS21
Subjects: Programming Languages (cs.PL)
Cite as: arXiv:2107.09472 [cs.PL]
  (or arXiv:2107.09472v1 [cs.PL] for this version)

Submission history

From: Lucas Franceschino [view email]
[v1] Tue, 20 Jul 2021 13:24:43 GMT (69kb)
[v2] Sun, 17 Oct 2021 20:22:44 GMT (460kb,D)

Link back to: arXiv, form interface, contact.