The trace partitioning abstract domain
Top Cited Papers
- 2 August 2007
- journal article
- research article
- Published by Association for Computing Machinery (ACM) in ACM Transactions on Programming Languages and Systems
- Vol. 29 (5) , 26
- https://doi.org/10.1145/1275497.1275501
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.Keywords
This publication has 23 references indexed in Scilit:
- The octagon abstract domainHigher-Order and Symbolic Computation, 2006
- The Parallel Implementation of the Astrée Static AnalyzerPublished by Springer Nature ,2005
- The Arithmetic-Geometric Progression Abstract DomainPublished by Springer Nature ,2005
- Understanding the Origin of Alarms in AstréePublished by Springer Nature ,2005
- Static Analysis of Digital FiltersPublished by Springer Nature ,2004
- Design and Implementation of a Special-Purpose Static Program Analyzer for Safety-Critical Real-Time Embedded SoftwarePublished by Springer Nature ,2002
- Refining Static Analyses by Trace-Based Partitioning Using Control FlowPublished by Springer Nature ,1998
- Abstract Interpretation FrameworksJournal of Logic and Computation, 1992
- Abstract interpretation and application to logic programsThe Journal of Logic Programming, 1992
- Static analysis of arithmetical congruencesInternational Journal of Computer Mathematics, 1989