The Reduced Product of Abstract Domains and the Combination of Decision Procedures
The algebraic/model theoretic design of static analyzers uses abstract domains based on representations of properties and pre-calculated property transformers. It is very efficient. The logical/proof theoretic approach uses SMT solvers and computation on-the-fly of property transformers. It is very expressive. We propose a combination of the two approaches to reach the sweet spot best adapted to a specific application domain in the precision/cost spectrum. The proposed combination uses an iterated reduction to combine abstractions. The key observation is that the Nelson-Oppen procedure which decides satisfiability in a combination of logical theories by exchanging equalities and disequalities computes a reduced product (after the state is enhanced with some new “observations” corresponding to alien terms). By abandoning restrictions ensuring completeness (such as disjointness, convexity, stably-infiniteness or shininess, etc) we can even broaden the application scope of logical abstractions for static analysis (which is incomplete anyway). We also introduce a semantics based on multiple interpretations to deal with the soundness of that combinations on a formal basis.
- 1.Bertrane, J., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Rival, X.: Static analysis and verification of aerospace software by abstract interpretation. In: Infotech@Aerospace, pp. 2010–3385 (2010)Google Scholar
- 3.Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: 4th POPL, pp. 238–252 (1977)Google Scholar
- 4.Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: 6th POPL, pp. 269–282 (1979)Google Scholar
- 7.Ferrara, P., Logozzo, F., Fähndrich, M.: Safer unsafe code in.NET. In: OOPSLA, pp. 329–346 (2008)Google Scholar
- 13.McIlraith, S.A., Amir, E.: Theorem proving with structured theories. In: IJCAI, pp. 624–634 (2001)Google Scholar