index.tex

\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.
All the files distributed in the original package, except the files
contained in the ppl, products, examples, and test subdirectories, are
distributed under the GNU Lesser General Public License version 2.1
with an exception allowing the redistribution of statically linked
executables.
The files contained in the ppl, products, examples, and test subdirectories
are distributed under the GNU General Public License version 2.


\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}