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
module LaTeX.Entrypoint

module Prettier = LaTeX.Prettier

open Main
/// \documentclass{llncs}
/// \input{latex/preamble.tex}
/// 
/// \begin{document}
/// \maketitle{}
/// \input{latex/abstract.tex}
/// \input{latex/introduction.tex}

/// \section{$\IMP{}$: a Small Imperative Language}
//!open LangDef

/// \section{Operational Semantics}
/// \label{section:operational-sematic}
//!open OperationalSemantic

/// \section{Abstract Domains}
/// \label{abstract-domains}
//!open ADom

/// \section{An Example of Abstract Domain: Intervals}
/// \label{intervals}
//!open Interval
 
/// \section{Specialized Abstract Domains}
/// \label{specialized-adoms}

/// Abstract domains are defined in Section~\ref{abstract-domains} as
/// lattices equipped with a sound concretization operation.

/// Our abstract interpreter analyses $\IMP{}$ programs: its
/// expressions are numerical, and $\IMP{}$ is equipped with a memory.
/// Thus, this section defines two specialized abstract domains: one
/// for numerical abstractions, and another one for memory
/// abstractions.
 
/// \subsection{Numerical Abstract Domains}
//!open ADom.Num

/// \subsection{Memory Abstract Domains}
//!open ADom.Mem

/// \section{A Weakly-Relational Abstract Memory}
/// \label{amem}
//!open AMem
///
//!open AMem.ADom

/// \section{Statement Abstract Interpretation}
/// \label{asem-stmt}
//!open AbstractSemantic

/// \input{latex/related-work.tex}
/// \input{latex/conclusion.tex}
// List of hidden definitions:{ {hidden-report}};

/// \newpage
/// \printglossary[type=\acronymtype]
/// \bibliographystyle{latex/splncs04}
/// \bibliography{latex/main}
/// 
/// \end{document}