When designing a tractable static analysis, one usually needs to approximate the trace semantics. This paper proposes a systematic way of regaining some knowledge about the traces by performing the abstraction over a partition of the set of traces instead of the set itself. This systematic refinement is not only theoretical but tractable: we give automatic procedures to build pertinent partitions of the traces and show the efficiency on an implementation integrated in the Astrée static analyzer, a tool capable of dealing with industrial-size software.

@inproceedings{lmxr:esop05,
author = {L{.} Mauborgne and X{.} Rival},
title =  {Trace {P}artitioning in {A}bstract {I}nterpretation
          {B}ased {S}tatic {A}nalyzers},
booktitle =    {ESOP'05},
year = 	 {2005},