Related Work and Tools on Comparing Functional Equivalence

  1. Martín Abadi, Leslie Lamport, The existence of refinement mappings, Theoretical Computer Science 1991
  2. Armando Solar-Lezama, Gilad Arnold, Liviu Tancau, Rastislav Bodik, Vijay Saraswat and Sanjit Seshia, Sketching Stencils, PLDI 2007
  3. Sumit Gulwani, Sagar Jain, and Eric Koskinen, Control-Flow Refinement and Progress Invariants for Bound Analysis, PLDI 2009
  4. Roberto Segala, The Power of Simulation Relations, Proceedings of the twenty-seventh ACM symposium on Principles of distributed computing
  5. Idit Keidar, Roger Khazan, Nancy Lynch, Alex Shvarteman, An inheritance-based technique for building simulation proofs incrementally, ACM Transactions on Software Engineering and Methodology 2002
  6. Toh Ne Win, Michael D. Ernst, Stephen J. Garland, Dilsun Kırlı, Nancy A. Lynch, Using simulated execution in verifying distributed algorithms, International Journal on Software Tools for Technology Transfer 2002
  7. Clark Barrett, Yi Fang, Benjamin Goldberg, Ying Hu, Amir Pnueli, and Lenore Zuck, TVOC: A Translation Validator for Optimizing Compilers, CAV 2005
    • URL: http://www.springerlink.com/content/8v65w0080vchcwjw/
    • Summary: This paper described a tool called TVOC to check the validity of compiler optimizations by using the translation validation approach. It proves the equivalence of the source code and the target code produced by running the compiler. The tool achieves this goal through two phases. First, it tries to reorder the transformations to make the corresponding loops in two programs have similar structures. Second, TVOC will try to handle the structure-preserving transformation by using cut-points, control mappings and data mappings. It will automatically generate the conditions and different paths between cut-points and try to determine whether the values of the variables in the data mappings are preserved. It introduced the notion of observable variables whose values must be preserved through the whole execution. It is a prototype tool and hasn't support procedures(functions) and pointers yet. The website also doesn't show any sign of update from 2005.
  8. Sven Verdoolaege, Gerda Janssens, and Maurice Bruynooghe, Equivalence Checking of Static Affine Programs Using Widening to Handle Recurrences, CAV 2009
  9. Lenore Zuck, Amir Pnueli, Benjamin Goldberg, Translation Validation of Loop Optimizations in Optimizing Compilers,
  10. Cristian Cadar, Daniel Dunbar, Dawson Engler, KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs, Proc. 8th USENIX Symposium on Operating Systems Design and Implementation (OSDI 2008)
    • URL: http://llvm.org/pubs/2008-12-OSDI-KLEE.pdf
    • Summary:This paper described the symbolic execution tool KLEE, which is capable of automatically generating test to achieve high test coverage. The tool used several optimizations to achieve high performance, including compact state representation, query optimization and coverage-optimized search. KLEE modeled the external environment, e.g command-line arguments, file data, network packet, etc, by redirecting the environment calls to models that understand the semantics of these calls and then these models will take actions. KLEE is also able to check the equivalence between functions on a finite set of explored paths. The result is conservative, e.g, the equivalence is only hold on the finite set of paths that KLEE explores. Experimental results on several real world test suite and benchmarks are given.
  11. Lenore Zuck, Amir Pnueli, Benjamin Goldberg, Clark Barrett, Yi Fang, Ying Hu, Translation and Run-Time Validation of Loop Transformations
    • URL: http://www.springerlink.com/content/p2kv2n73u6551132/
    • Summary: This paper presents new approaches to the validation of loop optimizations used by compilers. It introduced the permutation rules for loop reordering transformation and illustrated the idea with examples. The next part of the paper discuss the translation validation of structure preserving optimizations by formally define a transition system first and then define the validate proof rule on the system and prove it. The paper also gave an overview of the run-time validation of speculative optimizations. This paper mainly focuses on different loop optimizations and apply only to sequential programs.
  12. Ying Hu, Clark Barrett, Benjamin Goldberg, Amir Pnueli, Validating More Loop Optimizations,
  13. Suzette Person, Matthew B. Dwyer, Sebastian Elbaum, Corina S. Pa ̆sa ̆reanu, Differential Symbolic Execution, Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of software engineering, 2008
  14. K.C. Shashidhar, Maurice Bruynooghe, Francky Catthoor, Gerda Janssens, Functional Equivalence Checking for Verification of Algebraic Transformations on Array-Intensive Source Code, Proceedings of the conference on Design, Automation and Test in Europe - Volume 2 2005
    • URL: http://portal.acm.org/citation.cfm?id=1049316
    • Summary: This paper presents a verification tool for checking functional equivalence between a program and its transformed counterpart. It focuses on loop transformation, e.g, reordering of loop indices or reforming loop structure, and on algebraic transformation. The tool takes C programs as input and converts these programs into some certain format (single assignment form, free of pointer arithmetic, etc.) Then it uses a structure called Array Data Dependence Graph (ADDG) to facilitate the equivalence checking process. This tool can only handle sequential programs.
  15. K.C. Shashidhar, Maurice Bruynooghe, Francky Catthoor, Gerda Janssens, Verification of Source Code Transformations by Program Equivalence Checking, 2005
  16. Prateek Saxena, Pongsin Poosankam, Stephen McCamant, Dawn Song, Loop-Extended Symbolic Execution on Binary Programs, ISSTA 2009
  17. Peter H. Schmitt and Benjamin Weiß, Inferring Invariants by Symbolic Execution, 4th International Verification Workshop, 2007
    • URL: http://scholar.google.com/scholar?hl=en&q=Inferring+Invariants+by+Symbolic+Execution&btnG=Search&as_sdt=10000&as_ylo=&as_vis=0
    • Summary: This paper proposed a method for inferring invariants for loops in Java programs to facilitate verification. It used symbolic execution with abstract interpretation on loop constructs to infer loop invariants. Several rules are formally defined and applied to the method. The paper also gave execution results of the implementation of this method. However, the result doesn't seem very powerful (over 8min on a relatively simple selection sort example) and it also suffered the problem of dominating running time of the theorem prover. Also the produced loop invariants are long and complicated, thus hard for users to check.
  18. F. Ivančić, Z. Yang, M.K. Ganai, A. Gupta1, I. Shlyakhter and P. Ashar, F-Soft: Software Verification Platform, CAV 2005
  19. Edmund Clarke, Daniel Kroening, and Flavio Lerda, A Tool for Checking ANSI-C Programs, TACAS 2004
  20. Jean-Christophe Filliaˆtre and Claude March ́e, The Why/Krakatoa/Caduceus Platform for Deductive Program Verification, CAV 2007
    • URL: http://www.springerlink.com/content/47264171w71732qj/
    • Summary: This paper described the Why/Krakatoa/Caduceus set of tools for deductive verification of Java and C source code. The Krakatoa serves as the front-end for taking Java input and the Caduceus is the front-end for C program. Within these two front-ends, the source programs are translated to the intermediate program called the Why program. Then the verification conditions are extracted from Why programs and fed to provers. This platform supports multi-source and multi-prover. The verification requirements are written in JML or special format C comment. Hence it requires manual written annotations.
  21. Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar and Gr ́egoire SutreSoftware Verification with BLAST, SPIN 2003
    • URL: http://www.springerlink.com/content/r5xy1apqk8fpxf6a/
    • Summary: This paper briefly introduce BLAST, a verification system, developed at UC-Berkeley, for checking C programs. BLAST uses automatic property-driven construction and model checking of software abstractions to facilitate the verification process. The inputed C programs are represented as Control Flow Automata (CFA) internally and the verification process is based on a reachability search. To reach better performance, several optimizations are used by BLAST to reduce the interaction time between it and the theorem prover. BLAST is a tool for sequential programs.
  22. Mark Stewart, Advancing Scientific Computation by Improving Scientific Code Development: Symbolic Execution and Semantic Analysis, ICCS 2005
  23. Ofer Strichman and Benny Godlin, Regression Verification - A Practical Way to Verify Programs, IFIP 2008
    • URL: http://www.springerlink.com/content/hm326p82g8430p26/
    • Summary: This paper proposed a method to verify the equivalence between programs by the way of regression verification. An initial and simple version of the program is verified, and as the program is developed or optimized, the regression tool is applied to the modified program repeatedly. And if the new program produce a different result with the old one, the user has to specify whether this difference comes from an intended change or a bug. For this method, regular user interventions are required, either for identifying the difference between programs or to help the tool to tell intended changes from real bugs. The paper also proposed a series of challenges that the method is facing. The tool is in its early stage and hasn't address several important issues such as recursive function calls and pointer type function argument.
  24. Takeshi Matsumoto, Hiroshi Saito, and Masahiro Fujita, Equivalence Checking of C Programs by Locally Performing Symbolic Simulation on Dependence Graphs, ISQED 2006
    • URL: http://portal.acm.org/citation.cfm?id=1126255.1126780
    • Summary: This paper proposed a method to verify the equivalence between two C programs. The method tends to conduct the verification in an incremental manner. It first identifies the differences between the two programs and tries to verify these differences. If it fails to do so, the method will increase the area of verification based on dependence graph until either it succeeds or the primary output variables are proved to be inequivalent or it reaches the start/end of the programs. So in the worst case, the whole programs may still be involved in the verification process, which may cause the traditional infinite state space problem. Another restriction of this method is that it requires that the programs are free of pointers, dynamic memory allocation and recursive function calls, which affects the strength of this method. Also, the paper didn't mention much about how to check the equivalence between sequential and parallel programs by using this method.
  25. James C. King, Symbolic Execution and ProgramTesting, ACM Comm. 1976
  26. Sarfraz Khurshid, Corina S. Pa ̆s ̆areanu, and Willem Visser, Generalized Symbolic Execution for Model Checking and Testing, TACAS 2003
  27. Saswat Anand, Corina S. Pa ̆s ̆areanu, and Willem Visser, Symbolic Execution with Abstract Subsumption Checking, SPIN 2006
  28. Xianghua Deng, Jooyong Lee, Robby, Bogor/Kiasan: A k-bounded Symbolic Execution for Checking Strong Heap Properties of Open Systems, ASE 2006
  29. Corina S. Pa ̆s ̆areanu and Willem Visser, Verification of Java Programs Using Symbolic Execution and Invariant Generation, SPIN 2004
  30. Benny Godlin and Ofer Strichman, Inference rules for proving the equivalence of recursive procedures, Acta Informatica 2008
  31. Jiří Barnat1, Luboš Brim, Ivana Černá, Pavel Moravec, Petr Ročkai and Pavel Šimeček, DiVinE – A Tool for Distributed Verification, CAV 2006
  32. Manuvir Das, Sorin Lerner, Mark Seigle, ESP: path-sensitive program verification in polynomial time, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation
  33. Jean-Christophe Filliaˆtre and Claude Marche , Multi-prover Verification of C Programs, ICFEM 2004
  34. Siegel, S.F., Mironova, A., Avrunin, G.S., Clark, L.A., Combining Symbolic Execution with Model Checking to Verify Parallel Numerical Programs, ACM Trans. on Software Engineering and Methodology 2008
  35. Stephen F. Siegel, Model Checking Nonblocking MPI Programs, VMCAI 2007
  36. Sarvani Vakkalanka, Subodh Sharma, Ganesh Gopalakrishnan, Robert M. Kirby, ISP: a tool for model checking MPI programs, Proceedings of the 13th ACM SIGPLAN Symposium on Principles and practice of parallel programming 2008
  37. Daniel Kroening and Georg Weissenbacher, Verification and falsification of programs with loops using predicate abstraction, Formal Aspected of Computing, April 2009
  38. Shuyi Shao, Yu Zhang, Alex K. Jones, Rami Melhem, Symbolic Expression Analysis for Compiled Communication, Parallel Processing Letters, 2008