Automated Discovery of Simulation Between Programs
Abstract
Deciding equivalence between two programs (called a source and a target program) is often reduced to finding a simulation relation between them. This is computationally expensive and often requires a manual guidance. In this paper, we propose an abstraction-refinement-guided approach, called SimAbs, to automatically construct a simulation relation between the source program and an abstraction of the target program. In our approach both the abstraction and the simulation relation are discovered automatically, and deciding whether a given relation is a simulation relation is reduced to deciding validity of a AE-formula. We present a novel algorithm for deciding such formulas using an SMT-solver. In addition to deciding validity, our algorithm constructs a witnessing Skolem relation. These relations enable the refinement-step of SimAbs. We have implemented SimAbs using UFO framework and Z3 SMT-solver and applied it to finding simulation relations between C programs from the Software Verification Competition. Our empirical results show that SimAbs is efficient at finding a simulation relation.
Document Details
- Document Type
- Technical Report
- Publication Date
- Oct 18, 2014
- Accession Number
- ADA613949
Entities
People
- Arie Gurfinkel
- Grigory Fedyukovich
- Natasha Sharygina
Organizations
- Carnegie Mellon University