Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
International Journal on Software Tools for Technology Transfer
Published in: International Journal on Software Tools for Technology Transfer 4/2016

01-08-2016 | SPIN 2013

Automatic equivalence checking of programs with uninterpreted functions and integer arithmetic

Authors: Nuno P. Lopes, José Monteiro

Published in: International Journal on Software Tools for Technology Transfer | Issue 4/2016

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

Proving equivalence of programs has several important applications, including algorithm recognition, regression checking, compiler optimization verification and validation, and information flow checking. Despite being a topic with so many important applications, program equivalence checking has seen little advances over the past decades due to its inherent (high) complexity. In this paper, we propose, to the best of our knowledge, the first semi-algorithm for the automatic verification of partial equivalence of two programs over the combined theory of uninterpreted function symbols and integer arithmetic (UF+IA). The proposed algorithm supports, in particular, programs with nested loops. The crux of the technique is a transformation of uninterpreted functions (UFs) applications into integer polynomials, which enables the precise summarization of loops with UF applications using recurrences. The equivalence checking algorithm then proceeds on loop-free, integer only programs. We implemented the proposed technique in CORK, a tool that automatically verifies the correctness of compiler optimizations, and we show that it can prove more optimizations correct than state-of-the-art techniques.
previous article Preface of the special issue on Model Checking of Software
next article Model checking unbounded concurrent lists

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now
Appendix
Available only for authorised users
Footnotes
1
As an anecdote, when developing this example, we forgot the \(\mathbf{if } \) command in the program on the right. Fortunately, our prototype quickly pointed out our mistake (of different values of \(i\) at the end of the programs when the loops do not execute).
 
2
 
Literature
1.
Aho, A.V., Lam, M.S., Sethi, R., Ullman, J.D.: Compilers: principles, techniques, and tools, 2nd edn. Addison-Wesley (2006)
2.
Albarghouthi, A., Li, Y., Gurfinkel, A., Chechik, M.: UFO: a frame work for abstraction-and interpolation-based software verification. In: Proceedings of the 24th International Conference on Computer Aided Verification. Springer, Berlin, Heidelberg (2012)
3.
Alias, C., Barthou, D.: On the recognition of algorithm templates. In: Proceedings of the 2nd International Workshop on Compiler Optimization Meets Compiler Verification. Elsevier, Amsterdam (2003)
4.
Ball, T., Rajamani, S.K.: The SLAM project: debugging system software via static analysis. In: Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ACM, New York (2002)
5.
Barthe, G., D’Argenio, P.R., Rezk, T.: Secure information flow by self-composition. In: Proceedings of the 17th IEEE Workshop on Computer Security Foundations. IEEE Computer Society, Washington (2004)
6.
Barthe, G., Crespo, J.M., Kunz, C.: Relational verification using product programs. In: Proceedings of the 17th International Conference on Formal Methods. Springer, Berlin, Heidelberg (2011)
7.
Barthou, D., Feautrier, P., Redon, X.: On the equivalence of two systems of affine recurrence equations. In: Proceedings of the 8th International Euro-Par Conference on Parallel Processing. Springer, Berlin, Heidelberg (2002)
8.
Benton, N.: Simple relational correctness proofs for static analyses and program transformations. In: Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM, New York (2004)
9.
Bertot, Y., Castéran, P.: Interactive theorem proving and program development. Coq’Art: the calculus of inductive constructions. Springer–Verlag (2004)
10.
Beyer, D., Keremoglu, M.E.: CPAchecker: a tool for configurable software verification. In: Proceedings of the 23rd International Conference on Computer Aided Verification. Springer, Berlin, Heidelberg (2011)
11.
Beyer, D., Henzinger, T.A., Majumdar, R., Rybalchenko, A.: Invariant synthesis for combined theories. In: Proceedings of the 8th International Conference on Verification, Model Checking, and Abstract Interpretation. Springer, Berlin, Heidelberg (2007)
12.
Blanc, R., Henzinger, T.A., Hottelier, T., Kovács, L.: ABC: algebraic bound computation for loops. In: Proceedings of the 16th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning. Springer, Berlin, Heidelberg (2010)
13.
Bozga, M., Iosif, R., Konečný, F.: Fast acceleration of ultimately periodic relations. In: Proceedings of the 22nd International Conference on Computer Aided Verification. Springer, Berlin, Heidelberg (2010)
14.
Cachera, D., Jensen, T., Jobin, A., Kirchner, F.: Inference of polynomial invariants for imperative programs: a farewell to Gröbner bases. In: Proceedings of the 19th International Conference on Static Analysis. Springer, Berlin, Heidelberg (2012)
15.
Cadar, C., Dunbar, D., Engler, D.: KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation. USENIX Association, Berkeley (2008)
16.
Cahen, P.-J., Chabert, J.-L.: Integer-valued polynomials. In: Mathematical Surveys and Monographs. vol. 48. American Mathematical Society, Rhode Island (1997)
17.
18.
Caniart, N., Fleury, E., Leroux, J., Zeitoun, M.: Accelerating interpolation-based model-checking. In: Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, Berlin, Heidelberg (2008)
19.
Chaki, S., Gurfinkel, A., Strichman, O.: Regression verification for multi-threaded programs. In: Proceedings of the 13th International Conference on Verification, Model Checking, and Abstract Interpretation. Springer, Berlin, Heidelberg (2012)
20.
Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Proceedings of the 5th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages. ACM, New York (1978)
21.
Dai, L., Xia, B., Zhan, N.: Generating non-linear interpolants by semidefinite programming. In: Proceedings of the 25th International Conference on Computer Aided Verification. Springer, Berlin, Heidelberg (2013)
22.
de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, Berlin, Heidelberg (2008)
23.
Dissegna, S., Logozzo, F., Ranzato, F.: Tracing compilation by abstract interpretation. In: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM, New York (2014)
24.
25.
26.
Godlin, B., Strichman, O.: Inference rules for proving the equivalence of recursive procedures. Acta Inform. 45(6), 403–439 (2008)MathSciNetCrossRefMATH
27.
Godlin, B., Strichman, O.: Regression verification. In: Proceedings of the 46th Annual Design Automation Conference. IEEE Computer Society, Washington (2009)
28.
Goldberg, B., Zuck, L., Barrett, C.: Into the loops: practical issues in translation validation for optimizing compilers. Electron. Notes Theor. Comput. Sci. 132(1), 53–71 (2005)CrossRef
29.
Gonnord, L., Schrammel, P.: Abstract acceleration in linear relation analysis. Sci. Comput. Program. 93, 125–153 (2014)
30.
Grebenshchikov, S., Lopes, N.P., Popeea, C., Rybalchenko, A.: Synthesizing software verifiers from proof rules. In: Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM, New York (2012)
31.
Gulwani, S., Tiwari, A.: Assertion checking over combined abstraction of linear arithmetic and uninterpreted functions. In: Proceedings of the 15th European Conference on Programming Languages and Systems. Springer, Berlin, Heidelberg (2006)
32.
Gulwani, S., Mehra, K.K., Chilimbi, T.: SPEED: precise and efficient static estimation of program computational complexity. In: Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM, New York (2009)
33.
Gulwani, S., Srivastava, S., Venkatesan, R.: Constraint-based invariant inference over predicate abstraction. In: Proceedings of the 10th International Conference on Predicate Abstraction. Springer, Berlin, Heidelberg (2009)
34.
Guo, S.-Y., Palsberg, J.: The essence of compiling with traces. In: Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM, New York (2011)
35.
Gupta, A., Popeea, C., Rybalchenko, A.: Solving recursion-free horn clauses over LI+UIF. In: Proceedings of the 9th Asian Conference on Programming Languages and Systems. Springer, Berlin, Heidelberg (2011)
36.
Hawblitzel, C., Kawaguchi, M., Lahiri, S.K., Rebêlo, H.: Towards modularly comparing programs using automated theorem provers. In: Proceedings of the 24th International Conference on Automated Deduction. Springer, Berlin, Heidelberg (2013)
37.
Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM, New York (2004)
38.
Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM, NewYork (2002)
39.
Hojjat, H., Iosif, R., Konečný, F., Kuncak, V., Rümmer, P.: Accelerating interpolants. In: Proceedings of the 10th International Conference on Automated Technology for Verification and Analysis. Springer, Berlin, Heidelberg (2012)
40.
Jhala, R., Majumdar, R.: Software model checking. ACM Comput. Surv. 41(4), 21:1–21:54 (2009)CrossRef
41.
Kundu, S., Tatlock, Z., Lerner, S.: Proving optimizations correct using parameterized program equivalence. In: Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM, New York (2009)
42.
Lahiri, S.K., Hawblitzel, C., Kawaguchi, M., Rebêlo, H.: SymDiff: a language-agnostic semantic diff tool for imperative programs. In: Proceedings of the 24th International Conference on Computer Aided Verification. Springer, Berlin, Heidelberg (2012)
43.
Le, V., Afshari, M., Su, Z.: Compiler validation via equivalence modulo inputs. In: Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM, New York (2014)
44.
Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107–115 (2009)CrossRef
45.
Li, Y., Albarghouthi, A., Kincaid, Z., Gurfinkel, A., Chechik, M.: Symbolic optimization with SMT solvers. In: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM, New York (2014)
46.
Liang, H., Feng, X., Fu, M.: A rely-guarantee-based simulation for verifying concurrent program transformations. In: Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM, New York (2012)
47.
Lopes, N.P., Monteiro, J.: Automatic equivalence checking of UF+IA programs. In: Proceedings of the 20th International SPIN Symposium on Model Checking of Software. Springer, Berlin, Heidelberg (2013)
48.
Lopes, N.P., Monteiro, J.: Weakest precondition synthesis for compiler optimizations. In: Proceedings of the 15th International Conference on Verification, Model Checking, and Abstract Interpretation. Springer, Berlin, Heidelberg (2014)
49.
Matsumoto, T., Saito, H., Fujita, M.: Equivalence checking of C programs by locally performing symbolic simulation on dependence graphs. In: Proceedings of the 7th International Symposium on Quality Electronic Design. IEEE Computer Society, Washington (2006)
50.
McMillan, K.L.: Interpolants from Z3 proofs. In: Proceedings of the International Conference on Formal Methods in Computer-Aided Design. Springer, Berlin, Heidelberg (2011)
51.
McMillan, K.L., Rybalchenko, A.: Computing relational fixed points using interpolation. Technical Report MSR-TR-2013-6 (2013)
52.
Muchnick, S.S.: Advanced compiler design and implementation. Morgan Kaufmann, San Francisco (1997)
53.
54.
Namjoshi, K.S., Zuck, L.D.:Witnessing program transformations. In: Proceedings of the 20th International Conference on Static Analysis. Springer, Berlin, Heidelberg (2013)
55.
Necula, G.C.: Translation validation for an optimizing compiler. In: Proceedings of the ACM SIGPLAN 2000 Conference on Programming Language Design and Implementation. ACM, New York (2000)
56.
57.
Person, S., Dwyer, M.B., Elbaum, S., Pǎsǎreanu, C.S.: Differential symbolic execution. In: Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of Software Engineering. ACM, New York (2008)
58.
Pnueli, A., Siegel, M., Singerman, E.: Translation validation. In: Proceedings of the 4th International Conference on Tools and Algorithms for Construction and Analysis of Systems. Springer, Berlin, Heidelberg (1998)
59.
Ramos, D.A., Engler, D.R.: Practical, low-effort equivalence verification of real code. In: Proceedings of the 23rd International Conference on Computer Aided Verification. Springer, Berlin, Heidelberg (2011)
60.
Rodríguez-Carbonell, E., Kapur, D.: Generating all polynomial invariants in simple loops. J. Symb. Comput. 42(4), 443–476 (2007)MathSciNetCrossRefMATH
61.
Rybalchenko, A., Sofronie-Stokkermans, V.: Constraint solving for interpolation. In: Proceedings of the 8th International Conference on Verification, Model Checking, and Abstract Interpretation. Springer, Berlin, Heidelberg (2007)
62.
Sangiorgi, D.: On the origins of bisimulation and coinduction. ACM Trans. Program. Lang. Syst. 31(4), 15:1–15:41 (2009)
63.
Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Non-linear loopinvariant generation using Gröbner bases. In: Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM, New York (2004)
64.
Sharma, R., Dillig, I., Dillig, T., Aiken, A.: Simplifying loop invariant generation using splitter predicates. In: Proceedings of the 23rd International Conference on Computer Aided Verification. Springer, Berlin, Heidelberg (2011)
65.
Shashidhar, K.C., Bruynooghe, M., Catthoor, F., Janssens, G.: Verification of source code transformations by program equivalence checking. In: Proceedings of the 14th International Conference on Compiler Construction. Springer, Berlin, Heidelberg (2005)
66.
Stepp, M., Tate, R., Lerner, S.: Equality-based translation validator for LLVM. In: Proceedings of the 23rd International Conference on Computer Aided Verification. Springer, Berlin, Heidelberg (2011)
67.
Strang, G.: Linear algebra and its applications, 2nd edn. Academic Press, New York (1980)
68.
Tatlock, Z., Lerner, S.: Bringing extensibility to verified compilers. In: Proceedings of the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM, New York (2010)
69.
Terauchi, T.: Aiken, A.: Secure information flow as a safety problem. In: Proceedings of the 12th International Conference on Static Analysis. Springer, Berlin, Heidelberg (2005)
70.
Tristan, J.-B., Govereau, P., Morrisett, G.: Evaluating value-graph translation validation for LLVM. In: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM, New York (2011)
71.
Verdoolaege, S., Janssens, G., Bruynooghe, M.: Equivalence checking of static affine programs using widening to handle recurrences. In: Proceedings of the 21st International Conference on Computer Aided Verification. Springer, Berlin, Heidelberg (2009)
72.
Yang, X., Chen, Y., Eide, E., Regehr, J.: Finding and understanding bugs in C compilers. In: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM, New York (2011)
73.
Zaks, A., Pnueli, A.: CoVaC: Compiler validation by program analysis of the cross-product. In: Proceedings of the 15th International Symposium on Formal Methods. Springer, Berlin, Heidelberg (2008)
74.
Zhao, J., Nagarakatte, S., Martin, M.M.K., Zdancewic, S.: Formal verification of SSA-based optimizations for LLVM. In: Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM, New York (2013)
75.
Zuck, L., Pnueli, A., Goldberg, B., Barrett, C., Fang, Y., Hu, Y.: Translation and run-time validation of loop transformations. Form. Methods Syst. Des. 27(3), 335–360 (2005)
Metadata
Title
Automatic equivalence checking of programs with uninterpreted functions and integer arithmetic
Authors
Nuno P. Lopes
José Monteiro
Publication date
01-08-2016
Publisher
Springer Berlin Heidelberg
Published in
International Journal on Software Tools for Technology Transfer / Issue 4/2016
Print ISSN: 1433-2779
Electronic ISSN: 1433-2787
DOI
https://doi.org/10.1007/s10009-015-0366-1

Other articles of this Issue 4/2016

International Journal on Software Tools for Technology Transfer 4/2016 Go to the issue

SPIN 2013

Guided search for hybrid systems based on coarse-grained space abstractions

SPIN 2013

Model checking unbounded concurrent lists

SPIN 2013

Verifying a quantitative relaxation of linearizability via refinement

SPIN 2013

Guard-based partial-order reduction

Introduction

Preface of the special issue on Model Checking of Software

SPIN 2013

Efficient model-checking of weighted CTL with upper-bound constraints

Premium Partner

    Image Credits