1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
\section{Conclusion and further works}%
\label{conclusion}%

We presented almost the entire code of our abstract interpreter for $\IMP{}$.
%
Our approach to abstract interpretation is concretization-based, and
follows the methodology of~\cite{SAS13:Blazy:al,POPL15:Jourdan:al}.
%
While using \gls{fstar}, we did not encountered any issue regarding
expressivity, and additionally gained a lot in proof automatization,
to finally implement a fairly modular abstract interpreter.
The table below compares the line-of-proof vs. line-of-code ratio of
our implementation compared to some of the available verified abstract
interpreters.
%
Ours is up to 17 times more proof efficient.
%
It is very compact, and requires a negligible amount of manual proofs.
%
These formalizations do not target the same programming
languages:~\cite{POPL15:Jourdan:al} and~\cite{SAS13:Blazy:al} handles
the full C language, while~\cite{ITP10:Cachera:Pichardie} and the
curent paper only deal with an imperative language.

\begin{table}%{l}{0.5\textwidth}
  \centering%
  \setlength{\tabcolsep}{2mm}
  \begin{tabular}{rrrcl}
     & Code & Proof & Ratio\\
    \hline
    This paper
    & 487   & 39    & 0.08
    \\
    Pichardie et al.~\cite{ITP10:Cachera:Pichardie}
    & 3\,725  & 5\,020  & 1.35
    \\
    Verasco~\cite{POPL15:Jourdan:al}
    & 16\,847 & 17\,040 & 1.01
    \\
    Blazy et al.~\cite{SAS13:Blazy:al}
    & 4\,000  & 3\,500  & 0.87
  \end{tabular}%
\end{table}


The sources of our abstract interpreter sources are available along
with a set of example programs; building it natively or as a web
application is easy, reproducible\footnote{
  Our build process relies on the purely functional Nix package manager.%
} and automated.

This work is very far from the scope of Verasco which required about
four years of human
time~\cite{laporte:tel-01285624,jourdan:tel-01327023}, but our
results, which required 3 months of work with \gls{fstar} expertise,
are very encouraging.

\paragraph{Further work} We aim at following the path of Verasco by adding
real-world features to our abstract interpreter and consider a more
realistic target language such as one of the CompCert C-like input
languages.
%
One of the weakenesses of Verasco is its efficiency. Using
\gls{lowstar}, a C DSL for \gls{fstar}, it is possible to write (with
a nontrivial additionnal effort related to \gls{lowstar}) a very
efficient C and formally verified abstract interpreter.
%
This development also opens the path for enriching \gls{fstar}
automation via verified abstract interpretation.