Abstract
This paper presents the foundations for using automated deduction technology in static program analysis. The central principle is the use of logical lattices – a class of lattices defined on logical formulas in a logical theory – in an abstract interpretation framework. Abstract interpretation over logical lattices, called logical interpretation, raises new challenges for theorem proving. We present an overview of some of the existing results in the field of logical interpretation and outline some requirements for building expressive and scalable logical interpreters.
The first author was supported in part by the National Science Foundation under grant ITR-CCR-0326540.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Alpern, B., Wegman, M.N., Zadeck, F.K.: Detecting equality of variables in programs. In: 15th Annual ACM Symposium on POPL, pp. 1–11 (1988)
Baader, F., Snyder, W.: Unification theory. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, ch. 8, vol. I, pp. 445–532. Elsevier, Amsterdam (2001)
Cousot, P.: Forward relational infinitary static analysis, Lecture Notes (2005), Available at http://web.mit.edu/afs/athena.mit.edu/course/16/16.399/www
Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: 4th Annual ACM Symposium on POPL, pp. 234–252 (1977)
Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: 6th ACM Symp. on POPL, pp. 269–282 (1979)
Flanagan, C., Rustan, K., Leino, M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: PLDI, pp. 234–245 (2002)
Gulwani, S., Necula, G.C.: A polynomial-time algorithm for global value numbering. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol. 3148, pp. 212–227. Springer, Heidelberg (2004)
Gulwani, S., Tiwari, A.: Assertion checking over combined abstraction of linear arithmetic and uninterpreted functions. In: Sestoft, P. (ed.) ESOP 2006 and ETAPS 2006. LNCS, vol. 3924, Springer, Heidelberg (2006)
Gulwani, S., Tiwari, A.: Combining abstract interpreters. In: PLDI (June 2006)
Gulwani, S., Tiwari, A.: Assertion checking unified. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, Springer, Heidelberg (to appear, 2007)
Gulwani, S., Tiwari, A.: Computing procedure summaries for interprocedural analysis. In: Proc. European Symp. on Programming, ESOP 2007. LNCS, Springer, Heidelberg (to appear, 2007)
Gulwani, S., Tiwari, A.: Static analysis of heap manipulating low-level software. In: CAV. LNCS, vol. 4590, Springer, Heidelberg (2007)
Gulwani, S., Tiwari, A., Necula, G.C.: Join algorithms for the theory of uninterpreted symbols. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol. 3328, pp. 311–323. Springer, Heidelberg (2004)
Karr, M.: Affine relationships among variables of a program. Acta Informatica 6, 133–151 (1976)
Mine, A.: The octagon abstract domain. Higher Order Symbol. Comput. 19(1), 31–100 (2006)
Müller-Olm, M., Rüthing, O., Seidl, H.: Checking Herbrand equalities and beyond. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 79–96. Springer, Heidelberg (2005)
Müller-Olm, M., Seidl, H.: A note on Karr’s algorithm. In: 31st International Colloquium on Automata, Languages and Programming, pp. 1016–1028 (2004)
Müller-Olm, M., Seidl, H.: Precise interprocedural analysis through linear algebra. In: 31st ACM Symposium on POPL, pp. 330–341 (January 2004)
Nelson, G., Oppen, D.: Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems 1(2), 245–257 (1979)
Plandowski, W.: Testing equivalence of morphisms on context-free languages. In: van Leeuwen, J. (ed.) ESA 1994. LNCS, vol. 855, pp. 460–470. Springer, Heidelberg (1994)
Reps, T.: On the sequential nature of interprocedural program-analysis problems. Acta Informatica 33(8), 739–757 (1996)
Rodriguez-Carbonell, E., Kapur, D.: An abstract interpretation approach for automatic generation of polynomial invariants. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol. 3148, Springer, Heidelberg (2004)
Rüthing, O., Knoop, J., Steffen, B.: Detecting equalities of variables: Combining efficiency with precision. In: Cortesi, A., Filé, G. (eds.) SAS 1999. LNCS, vol. 1694, pp. 232–247. Springer, Heidelberg (1999)
Shankar, N.: Little engines of proof. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol. 2391, pp. 1–20. Springer, Heidelberg (2002)
Sharir, M., Pnueli, A.: Two approaches to interprocedural data flow analysis. In: Program Flow Analysis: Theory and Applications, pp. 189–233. Prentice-Hall, Englewood Cliffs (1981)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Tiwari, A., Gulwani, S. (2007). Logical Interpretation: Static Program Analysis Using Theorem Proving. In: Pfenning, F. (eds) Automated Deduction – CADE-21. CADE 2007. Lecture Notes in Computer Science(), vol 4603. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-73595-3_11
Download citation
DOI: https://doi.org/10.1007/978-3-540-73595-3_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-73594-6
Online ISBN: 978-3-540-73595-3
eBook Packages: Computer ScienceComputer Science (R0)