-
Notifications
You must be signed in to change notification settings - Fork 2
/
index.tex
195 lines (161 loc) · 7.45 KB
/
index.tex
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
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
\documentclass[a4paper,11pt]{article}
\usepackage{hyperlatex}
\htmlcss{style.css}
\htmltitle{APRON numerical abstract domain library}
\htmlpanel{0}
\setcounter{htmlautomenu}{1}
\setcounter{htmldepth}{1}
\usepackage{xspace}
\T\usepackage{color}
\T\usepackage{pstricks,pst-node,pstcol}
\T\usepackage{graphicx}
\T\usepackage{mycolor}
\T\usepackage{amsmath}
\T\usepackage{amssymb}
\usepackage{url}
%\usepackage{frames}
\newcommand{\ocaml}{\xlink{OCaml}{http://www.caml.org}\xspace}
\newcommand{\mlgmpidl}{\xlink{MLGMPIDL}{http://www.inrialpes.fr/pop-art/people/bjeannet/mlxxxidl-forge/mlgmpidl/}\xspace}
\newcommand{\camlidl}{\xlink{CamlIDL}{http://caml.inria.fr/camlidl/}\xspace}
\newcommand{\interproc}{\xlink{Interproc}{http://pop-art.inrialpes.fr/interproc/interprocweb.cgi}\xspace}
\title{APRON numerical abstract domain library}
\date{}
\author{}
\begin{document}
%\xmlattributes*{img}{align="left"}
%\xlink{\htmlimg{http://devel.inria.fr/logo_inria.png}{INRIA}}{http://www.inria.fr}
\xmlattributes*{img}{align="RIGHT"}
\htmlimg{poster.gif}{poster}
\xlink{Home page}{http://apron.cri.ensmp.fr/}
\maketitle
\section{About}
The APRON library is dedicated to the static analysis of the
numerical variables of a program by Abstract Interpretation. The
aim of such an analysis is to infer invariants about these
variables. like $1<=x+y<=z$, which holds during any execution of
the program. You may look at to the \interproc analyzer for an
online demonstration of static analysis.
The APRON library is intended to be a common interface to various
underlying libraries/abstract domains and to provide additional
services that can be implemented independently from the underlying
library/abstract domain, as shown by the poster on the right
(presented at the SAS 2007 conference. You may also look at:
\begin{itemize}
\item the associated \xlink{flyer}{flyer.pdf};
\item a \xlink{15 minutes
presentation}{expose_jeannet_CAV09.pdf} made at CAV 2009
conference in Grenoble \cite{jeannetmine09};
\item a \xlink{detailed
presentation}{expose_mine_CEA_2007.pdf} by Antoine Min\'e.
\end{itemize}
Currently, APRON provides a C interface and an \ocaml interface.
There also exists a C++ interface, which is more experimental.
The version 0.9.11 (august 2012) contains 4 libraries and 5 abstract domains:
\begin{itemize}
\item The BOX intervals library
\item The OCT octagon library
\item The NEWPOLKA Convex Polyhedra and Linear Equalities library
\item The TAYLOR1PLUS zonotope abstract domain, provided by CEA LIST \cite{Ghorbal2009}
\end{itemize}
It also provides an optional interface to the \xlink{Parma Polyhedra Library}{http://www.cs.unipr.it/ppl/}, which adds
\begin{itemize}
\item the Convex Polyhedra and Linear Congruences (grid) domains
\item the reduced product of NewPolka convex polyhedra and PPL
linear congruences
\end{itemize}
\section{Demonstration}
The online \interproc static analyzer illustrates the use of the
APRON library in static analysis.
\section{License}
APRON is a free software under LGPL license, except the wrappers
related to the PPL library, which follows the GPL license of the
PPL library.
\section{Documentation}
\begin{itemize}
\item \xlink{Detailed presentation}{expose_mine_CEA_2007.pdf};
\item On-line \xlink{C interface}{http://apron.cri.ensmp.fr/library/0.9.11/apron/apron.html} and \xlink{OCaml interface}{http://apron.cri.ensmp.fr/library/0.9.11/mlapronidl/index.html};
\item \xlink{C pdf}{http://apron.cri.ensmp.fr/library/0.9.11/apron.pdf} or \xlink{OCaml pdf}{http://apron.cri.ensmp.fr/library/0.9.11/mlapronidl.pdf};
\item \xlink{C example}{http://apron.cri.ensmp.fr/library/0.9.11/example1.c} or \xlink{OCaml example 1}{http://apron.cri.ensmp.fr/library/0.9.11/mlexample1.ml}/\xlink{OCaml example 2}{http://apron.cri.ensmp.fr/library/0.9.11/mlexample2.ml}/\xlink{OCaml example 3}{http://apron.cri.ensmp.fr/library/0.9.11/mlexample3.ml}. For the
ML examples, they are almost identical, but the ones with the
higher numbers use higher-level functions to define affine
expressions and constraints.
\end{itemize}
\section{Download}
\subsection{Requirements}
\begin{itemize}
\item An ANSI C compiler (only gcc with ansi option has been
tested)
\item The \xlink{GMP}{http://www.swox.com/gmp/} library, version 4.2 or up, and the \xlink{MPFR}{http://www.mpfr.org/} library, version 2.2 or up;
\item Optionally, \xlink{Parma Polyhedra
Library}{http://www.cs.unipr.it/ppl/}, and
\xlink{GMP}{http://www.swox.com/gmp/} compiled with
\kbd{-enable-cxx} configuration option)
\item If you want the C++ interface (still experimental), GCC 4.1.2 or up
\item If you want to use the \ocaml interface, you need the \ocaml
system, version 3.11 or up, the \camlidl 1.05 stub code
generator for the OCaml interface, as well as GNU SED 4.1 or
up, and GNU m4 (if you download from subversion repository).
You also need \mlgmpidl, but it can be included if you opt for
the ``distribution'' version of APRON (see below).
\end{itemize}
\subsection{Current version: 0.9.11}
\begin{itemize}
\item \xlink{Changes}{http://apron.cri.ensmp.fr/library/Changes}
\item The best way is to access to the \xlink{SUBVERSION
REPOSITORY}{https://gforge.inria.fr/scm/viewvc.php/?root=apron},
by typing something like
\begin{quote}
\kbd{svn list svn://scm.gforge.inria.fr/svnroot/apron}
\end{quote}
If you want to download to the last committed version:
\begin{quote}
\kbd{svn co svn://scm.gforge.inria.fr/svnroot/apron/apron/trunk apron}
\end{quote}
If you want to access the distribution which references both APRON and MLGMPIDL (using subversion external links):
\begin{quote}
\kbd{svn co svn://scm.gforge.inria.fr/svnroot/apron/apron-dist/trunk apron-dist}
\end{quote}
(the old repository \kbd{http://svn.cri.ensmp.fr/svn/apron/} is
obsolete)
\end{itemize}
As the library may still contain subtle bugs, we strongly suggest
to be up-to-date with the most recent version.
\subsection{Older versions}
\begin{itemize}
\item 0.9.9 \xlink{Tar-gzipped
sources}{http://apron.cri.ensmp.fr/library/apron-0.9.9.tgz}
\item 0.9.8 \xlink{Tar-gzipped
sources}{http://apron.cri.ensmp.fr/library/apron-0.9.8.tgz}
\item 0.9.7 \xlink{Tar-gzipped
sources}{http://apron.cri.ensmp.fr/library/apron-0.9.7.tgz}
\item 0.9.6 \xlink{Tar-gzipped
sources}{http://apron.cri.ensmp.fr/library/apron-0.9.6.tgz}
\item 0.9.5 \xlink{Tar-gzipped
sources}{http://apron.cri.ensmp.fr/library/apron-0.9.5.tgz}
\item 0.9.4 \xlink{Tar-gzipped
sources}{http://apron.cri.ensmp.fr/library/apron-0.9.4.tgz}
\item 0.9.3 \xlink{Tar-gzipped
sources}{http://apron.cri.ensmp.fr/library/apron-0.9.3.tgz}
\item 0.9.2 \xlink{Tar-gzipped
sources}{http://apron.cri.ensmp.fr/library/apron-0.9.2.tgz}
\item 0.9.1 \xlink{Tar-gzipped
sources}{http://apron.cri.ensmp.fr/library/apron-0.9.1.tgz}
\item 0.9.0 \xlink{Tar-gzipped
sources}{http://apron.cri.ensmp.fr/library/apron-0.9.0.tgz}
\end{itemize}
%\bibliography{bib,jabref,mybib}
%\bibliographystyle{alpha}
\begin{thebibliography}{GGP09}
\bibitem[GGP09]{Ghorbal2009}
Khalil Ghorbal, Eric Goubault, and Sylvie Putot.
\newblock The zonotope abstract domain taylor1+.
\newblock In {\em Computer Aided Verification, CAV'09}, volume 5643 of {\em
LNCS}, 2009.
\bibitem[JM09]{jeannetmine09}
B.~Jeannet and A.~Min\'e.
\newblock {APRON}: A library of numerical abstract domains for static analysis.
\newblock In {\em Computer Aided Verification, CAV'2009}, volume 5643 of {\em
LNCS}, pages 661--667, 2009.
\newblock \url{http://apron.cri.ensmp.fr/library/}.
\end{thebibliography}
\end{document}