Résumé: 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.

Langue: Anglais