Trace partitioning in abstract interpretation based static analyzers

Abstract

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. © Springer-Verlag Berlin Heidelberg 2005.