Abstract
We revisit the connection between equality assertion checking in programs and unification that was recently described in [7]. Using a general formalization of this connection, we establish interesting connections between the complexity of assertion checking in programs and unification theory of the underlying program expressions. In particular, we show that assertion checking is: (a) PTIME for programs with nondeterministic conditionals that use expressions from a strict unitary theory, (b) coNP-hard for programs with nondeterministic conditionals that use expressions from a bitary theory, and (c) decidable for programs with disequality guards that use expressions from a convex finitary theory. These results generalize several recently published results and also establish several new results. In essence, they provide new techniques for backward analysis of programs based on novel integration of theorem proving technology in program analysis.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Baader, F., Snyder, W.: Unification theory. In: Handbook of Automated Reasoning, vol. 1, pp. 445–532. Elsevier Science, Amsterdam (2001)
Cousot, P.: Types as abstract interpretations. In: POPL, pp. 316–331 (1997)
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.: Refining model checking by abstract interpretation. Automated Software Engineering 6(1), 69–95 (1999)
Gulwani, S., Jojic, N.: Program verification as inference in belief networks. Technical Report MSR-TR-2006-98, Microsoft Research (July 2006)
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 & uninterpreted functions. In: Sestoft, P. (ed.) ESOP 2006 and ETAPS 2006. LNCS, vol. 3924, Springer, Heidelberg (2006)
Gulwani, S., Tiwari, A.: Assertion checking unified. MSR-TR-2006-99 (July 2006)
Gulwani, S., Tiwari, A.: Combining abstract interpreters. In: PLDI (June 2006)
Hindley, R.: The principal type-scheme of an object in combinatory logic. Trans. Amer. Math. Soc. 146, 29–60 (1969)
Karr, M.: Affine relationships among variables of a program. In: Acta Informatica, pp. 133–151. Springer, Heidelberg (1976)
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: Díaz, J., et al. (eds.) ICALP 2004. LNCS, vol. 3142, pp. 1016–1028. Springer, Heidelberg (2004)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gulwani, S., Tiwari, A. (2007). Assertion Checking Unified. In: Cook, B., Podelski, A. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2007. Lecture Notes in Computer Science, vol 4349. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-69738-1_26
Download citation
DOI: https://doi.org/10.1007/978-3-540-69738-1_26
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-69735-0
Online ISBN: 978-3-540-69738-1
eBook Packages: Computer ScienceComputer Science (R0)