Assertion checking over combined abstraction of linear arithmetic and uninterpreted functions

13Citations
Citations of this article
3Readers
Mendeley users who have this article in their library.

Abstract

This paper presents results on the problem of checking equality assertions in programs whose expressions have been abstracted using combination of linear arithmetic and uninterpreted functions, and whose conditionals are treated as non-deterministic. We first show that the problem of assertion checking for this combined abstraction is coNP-hard, even for loop-free programs. This result is quite surprising since assertion checking for the individual abstractions of linear arithmetic and uninterpreted functions can be performed efficiently in polynomial time. Next, we give an assertion checking algorithm for this combined abstraction, thereby proving decidability of this problem despite the underlying lattice having infinite height. Our algorithm is based on an important connection between unification theory and program analysis. Specifically, we show that weakest preconditions can be strengthened by replacing equalities by their unifiers, without losing any precision, during backward analysis of programs. © Springer-Verlag Berlin Heidelberg 2006.

Cite

CITATION STYLE

APA

Gulwani, S., & Tiwari, A. (2006). Assertion checking over combined abstraction of linear arithmetic and uninterpreted functions. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 3924 LNCS, pp. 279–293). https://doi.org/10.1007/11693024_19

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free