The trace partitioning abstract domain
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.
verification experimentation theory