The Trace Partitioning Abstract Domain

Xavier Rival and Laurent Mauborgne.
The Trace Partitioning Abstract Domain.
ACM Transactions on Programming Languages and Systems (TOPLAS), 29(5), 2007
Compressed PostScript (342K), DVI (277K), PDF (515K).
Abstract: In order to achieve better precision of abstract interpretation based static analysis, we introduce a new generic abstract domain, the trace partitioning abstract domain. We develop a theoretical framework allowing a wide range of instantiations of the domain, proving that all these instantiations give correct results. From this theoretical framework, we go into implementation details of a particular instance developed in the \astree static analyzer. We show how the domain is automatically configured in \astree and the gain and cost in terms of performance and precision.

\bibitem{rival:mauborgne07}
{\sc Rival, X. and Mauborgne, L.}
\newblock The Trace Partitioning Abstract Domain.
\newblock {\em ACM Transactions on Programming Languages and Systems (TOPLAS)
 29(5)}, (2007).

@article{rival:mauborgne07,
author = "Xavier Rival and Laurent Mauborgne",
title  = "The Trace Partitioning Abstract Domain",
journal = "ACM Transactions on Programming Languages and Systems (TOPLAS)",
year   = 2007,
volume = 29,
number = 5,
publisher = "ACM",
address = "New York, NY, USA",

}

Email: Laurent.Mauborgne@ens.fr