Abstract
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.
Chapter PDF
Similar content being viewed by others
References
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)
Bradley, A.R., Manna, Z.: The Calculus of Computation, Decision procedures with Applications to Verification. Springer, Heidelberg (2007)
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)
Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: 6th POPL, pp. 269–282 (1979)
Cousot, P., Cousot, R., Mauborgne, L.: Logical Abstract Domains and Interpretations. In: Nanz, S. (ed.) The Future of Engineering. Springer, Heidelberg (2010)
Elder, M., Gopan, D., Reps, T.: View-Augmented Abstractions. In: 2nd NSAD, ENTCS (2010)
Ferrara, P., Logozzo, F., Fähndrich, M.: Safer unsafe code in.NET. In: OOPSLA, pp. 329–346 (2008)
Granger, P.: Improving the results of static analyses of programs by local decreasing iterations. In: Shyamasundar, R.K. (ed.) FSTTCS 1992. LNCS, vol. 652, pp. 68–79. Springer, Heidelberg (1992)
Gulwani, S., Lev-Ami, T., Sagiv, M.: A combination framework for tracking partition sizes. In: 36th POPL, pp. 239–251 (2009)
Gulwani, S., McCloskey, B., Tiwari, A.: Lifting abstract interpreters to quantified logical domains. In: 35th POPL, pp. 235–246 (2008)
Gulwani, S., Necula, G.C.: Path-sensitive analysis for linear arithmetic and uninterpreted functions. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol. 3148, pp. 328–343. Springer, Heidelberg (2004)
Gulwani, S., Tiwari, A.: Combining abstract interpreters. In: PLDI, pp. 376–386 (2006)
McIlraith, S.A., Amir, E.: Theorem proving with structured theories. In: IJCAI, pp. 624–634 (2001)
Miné, A.: Field-sensitive value analysis of embedded C programs with union types and pointer arithmetics. In: LCTES, pp. 54–63 (2006)
Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. TOPLAS 1(2), 245–257 (1979)
Reps, T.W., Sagiv, S., Yorsh, G.: Symbolic implementation of the best transformer. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 252–266. Springer, Heidelberg (2004)
Shankar, N., Rueß, H.: Combining shostak theories. In: Tison, S. (ed.) RTA 2002. LNCS, vol. 2378, pp. 1–18. Springer, Heidelberg (2002)
Tinelli, C., Harandi, M.T.: A new correctness proof of the Nelson–Oppen combination procedure. In: Frontiers of Combining Systems, pp. 103–120. Kluwer Academic Publishers, Dordrecht (1996)
Tinelli, C., Ringeissen, C.: Unions of non-disjoint theories and combinations of satisfiability procedures. Theor. Comput. Sci. 290(1), 291–353 (2003)
Tinelli, P., Zarba, C.G.: Combining non-stably infinite theories. Electr. Notes Theor. Comput. Sci. 86(1) (2003)
Tiwari, A., Gulwani, S.: Logical interpretation: Static program analysis using theorem proving. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 147–166. Springer, Heidelberg (2007)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cousot, P., Cousot, R., Mauborgne, L. (2011). The Reduced Product of Abstract Domains and the Combination of Decision Procedures. In: Hofmann, M. (eds) Foundations of Software Science and Computational Structures. FoSSaCS 2011. Lecture Notes in Computer Science, vol 6604. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-19805-2_31
Download citation
DOI: https://doi.org/10.1007/978-3-642-19805-2_31
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-19804-5
Online ISBN: 978-3-642-19805-2
eBook Packages: Computer ScienceComputer Science (R0)