Article

Assertion checking over combined abstraction of linear arithmetic and uninterpreted functions

Authors:

Ashish TiwariAuthors Info & Claims

ESOP'06: Proceedings of the 15th European conference on Programming Languages and Systems

Pages 279 - 293

https://doi.org/10.1007/11693024_19

Published: 27 March 2006 Publication History

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.

References

[1]

B. Alpern, M. N. Wegman, and F. K. Zadeck. Detecting equality of variables in programs. In 15th Annual ACM Symposium on POPL, pages 1-11, 1988.

Digital Library

[2]

F. Baader and K. Schulz. Unification in the union of disjoint equational theories: Combining decision procedures. In 11th International Conference on Automated Deduction, volume 607 of LNAI, pages 50-65, 1992.

Digital Library

[3]

F. Baader and W. Snyder. Unification theory. In Handbook of Automated Reasoning, volume I, chapter 8, pages 445-532. Elsevier Science, 2001.

[4]

L. Bachmair, A. Tiwari, and L. Vigneron. Abstract congruence closure. J. of Automated Reasoning, 31(2):129-168, 2003.

Digital Library

[5]

C. W. Barrett, D. L. Dill, and J. R. Levitt. Validity checking for combinations of theories with equality. In First International Conference on Formal Methods in Computer-Aided Design, volume 1166 of LNCS, pages 187-201, 1996.

Digital Library

[6]

P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In 4th Annual ACM Symposium on POPL, pages 234-252, 1977.

Digital Library

[7]

P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of a program. In 5th ACM Symposium on POPL, pages 84-96, 1978.

Digital Library

[8]

S. Gulwani and G. C. Necula. Discovering affine equalities using random interpretation. In 30th Annual ACM Symposium on POPL, Jan. 2003.

Digital Library

[9]

S. Gulwani and G. C. Necula. Global value numbering using random interpretation. In 31st Annual ACM Symposium on POPL, Jan. 2004.

Digital Library

[10]

S. Gulwani and G. C. Necula. A polynomial-time algorithm for global value numbering. In Static Analysis Symposium, volume 3148 of LNCS, pages 212-227, 2004.

[11]

S. Gulwani and G. C. Necula. Precise interprocedural analysis using random interpretation. In 32nd Annual ACM Symposium on POPL, Jan. 2005.

Digital Library

[12]

S. Gulwani and A. Tiwari. Combining abstract interpreters. Submitted for publication, Nov. 2005.

[13]

S. Gulwani and A. Tiwari. Assertion checking over combined abstraction of linear arithmetic and uninterpreted functions. Technical Report MSR-TR-2006-01, Microsoft Research, Jan. 2006.

Digital Library

[14]

M. Karr. Affine relationships among variables of a program. In Acta Informatica, pages 133-151. Springer, 1976.

[15]

G. A. Kildall. A unified approach to global program optimization. In 1st ACM Symposium on POPL, pages 194-206, Oct. 1973.

Digital Library

[16]

M. Müller-Olm, O. Rüthing, and H. Seidl. Checking herbrand equalities and beyond. In VMCAI, volume 3385 of LNCS, pages 79-96. Springer, Jan. 2005.

Digital Library

[17]

M. Müller-Olm and H. Seidl. A note on Karr's algorithm. In 31st International Colloquium on Automata, Languages and Programming, pages 1016-1028, 2004.

[18]

M. Müller-Olm and H. Seidl. Precise interprocedural analysis through linear algebra. In 31st ACM Symposium on POPL, pages 330-341, Jan. 2004.

Digital Library

[19]

M. Müller-Olm and H. Seidl. Analysis of modular arithmetic. In European Symposium on Programming, pages 46-60, 2005.

Digital Library

[20]

G. Nelson and D. Oppen. Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems, 1(2):245-257, Oct. 1979.

Digital Library

[21]

M. Schmidt-Schauss. Unification in a combination of arbitrary disjoint equational theories. J. Symbolic Computation, 8(1-2):51-99, 1989.

Digital Library

Cited By

Mathur UMadhusudan PViswanathan M(2019)Decidable verification of uninterpreted programsProceedings of the ACM on Programming Languages10.1145/32903593:POPL(1-29)Online publication date: 2-Jan-2019
https://dl.acm.org/doi/10.1145/3290359
Lopes NMonteiro J(2016)Automatic equivalence checking of programs with uninterpreted functions and integer arithmeticInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-015-0366-118:4(359-374)Online publication date: 1-Aug-2016
https://dl.acm.org/doi/10.1007/s10009-015-0366-1
Tiwari A(2009)Combining equational reasoningProceedings of the 7th international conference on Frontiers of combining systems10.5555/1807707.1807712(68-83)Online publication date: 16-Sep-2009
https://dl.acm.org/doi/10.5555/1807707.1807712
Show More Cited By

Recommendations

Trace Abstraction-Based Verification for Uninterpreted Programs
Formal Methods
Abstract
The verification of uninterpreted programs is undecidable in general. This paper proposes to employ counterexample-guided abstraction refinement (CEGAR) framework for verifying uninterpreted programs. Different from the existing interpolant-based ...
Automatic abstraction in model checking
Sufficient preconditions for modular assertion checking
VMCAI'08: Proceedings of the 9th international conference on Verification, model checking, and abstract interpretation

Assertion checking is the restriction of program verification to validity of program assertions. It encompasses safety checking, which is program verification of safety properties, like memory safety or absence of overflows. In this paper, we consider ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

ESOP'06: Proceedings of the 15th European conference on Programming Languages and Systems

March 2006

342 pages

ISBN:354033095X

Editor:
Peter Sestoft
IT University of Copenhagen, Denmark

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 27 March 2006

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

11
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 07 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Mathur UMadhusudan PViswanathan M(2019)Decidable verification of uninterpreted programsProceedings of the ACM on Programming Languages10.1145/32903593:POPL(1-29)Online publication date: 2-Jan-2019
https://dl.acm.org/doi/10.1145/3290359
Lopes NMonteiro J(2016)Automatic equivalence checking of programs with uninterpreted functions and integer arithmeticInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-015-0366-118:4(359-374)Online publication date: 1-Aug-2016
https://dl.acm.org/doi/10.1007/s10009-015-0366-1
Tiwari A(2009)Combining equational reasoningProceedings of the 7th international conference on Frontiers of combining systems10.5555/1807707.1807712(68-83)Online publication date: 16-Sep-2009
https://dl.acm.org/doi/10.5555/1807707.1807712
Shankar N(2009)Automated deduction for verificationACM Computing Surveys10.1145/1592434.159243741:4(1-56)Online publication date: 9-Oct-2009
https://dl.acm.org/doi/10.1145/1592434.1592437
Zaks APnueli AKrishnamurthi SYoung M(2008)Program analysis for compiler validationProceedings of the 8th ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering10.1145/1512475.1512477(1-7)Online publication date: 9-Nov-2008
https://dl.acm.org/doi/10.1145/1512475.1512477
Magill SBerdine JClarke ECook B(2007)Arithmetic strengthening for shape analysisProceedings of the 14th international conference on Static Analysis10.5555/2391451.2391479(419-436)Online publication date: 22-Aug-2007
https://dl.acm.org/doi/10.5555/2391451.2391479
Gulwani STiwari A(2007)Assertion checking unifiedProceedings of the 8th international conference on Verification, model checking, and abstract interpretation10.5555/1763048.1763086(363-377)Online publication date: 14-Jan-2007
https://dl.acm.org/doi/10.5555/1763048.1763086
Gulwani STiwari A(2007)Computing procedure summaries for interprocedural analysisProceedings of the 16th European Symposium on Programming10.5555/1762174.1762199(253-267)Online publication date: 24-Mar-2007
https://dl.acm.org/doi/10.5555/1762174.1762199
Tiwari AGulwani S(2007)Logical InterpretationProceedings of the 21st international conference on Automated Deduction: Automated Deduction10.1007/978-3-540-73595-3_11(147-166)Online publication date: 17-Jul-2007
https://dl.acm.org/doi/10.1007/978-3-540-73595-3_11
Gulwani STiwari ASchwartzbach MBall T(2006)Combining abstract interpretersProceedings of the 27th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/1133981.1134026(376-386)Online publication date: 11-Jun-2006
https://dl.acm.org/doi/10.1145/1133981.1134026
Show More Cited By

View Options

View options

Figures

Tables

Media

View Table of Conten