Data-driven equivalence checking
Authors:
Open Access
- 29 October 2013
- conference paper
- Published by Association for Computing Machinery (ACM)
- Vol. 48 (10) , 391-406
Abstract
We present a data driven algorithm for equivalence checking of two loops. The algorithm infers simulation relations using data from test runs. Once a candidate simulation relation has been obtained, off-the-shelf SMT solvers are used to check whether the simulation relation actually holds. The algorithm is sound: insufficient data will cause the proof to fail. We demonstrate a prototype implementation, called DDEC, of our algorithm, which is the first sound equivalence checker for loops written in x86 assembly.Keywords
This publication has 30 references indexed in Scilit:
- Abstract Semantic Differencing for Numerical Programs2013
- Efficiently solving quantified bit-vector formulasFormal Methods in System Design, 2012
- WYSINWYXACM Transactions on Programming Languages and Systems, 2010
- The Daikon system for dynamic detection of likely invariantsScience of Computer Programming, 2007
- DenaliACM Transactions on Programming Languages and Systems, 2006
- Into the Loops: Practical Issues in Translation Validation for Optimizing CompilersElectronic Notes in Theoretical Computer Science, 2005
- Verification of Source Code Transformations by Program Equivalence CheckingLecture Notes in Computer Science, 2005
- Symbolic Implementation of the Best Transformer2004
- Fractal symbolic analysisACM Transactions on Programming Languages and Systems, 2003
- Compiler transformations for high-performance computingACM Computing Surveys, 1994