\begin{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.

%% \keywords{Abstract interpretation \and Functional programming \and
%%   Formal verification.}
\end{abstract}