Technical report detail

Automated Discovery of Simulation Between Programs

by Grigory Fedyukovich, Arie Gurfinkel, Natasha Sharygina


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 "forall-exists"-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.


Technical report 2014/05, October 2014

BibTex entry

@techreport{14automated, author = {Grigory Fedyukovich and Arie Gurfinkel and Natasha Sharygina}, title = {Automated Discovery of Simulation Between Programs}, institution = {University of Lugano}, number = {2014/05}, year = 2014, month = oct }
Allegati