Paper Info
Title
Inference rules for proving the equivalence of recursive procedures
Abstract
Inspired by Hoare’s rule for recursive procedures, we present three proof rules for the equivalence between recursive programs. The first rule can be used for proving partial equivalence of programs; the second can be used for proving their mutual termination; the third rule can be used for proving the equivalence of reactive programs. There are various applications to such rules, such as proving equivalence of programs after refactoring and proving backward compatibility.
Year
DOI
Venue
2010
10.1007/s00236-008-0075-2
Essays in Memory of Amir Pnueli
Keywords
DocType
Volume
recursive invocation,various application,mutual termination,recursive procedure,recursive program,proof rule,partial equivalence,inference rule,reactive program
Conference
45
Issue
ISSN
ISBN
6
1432-0525
3-642-13753-9
Citations 
PageRank 
References 
30
1.43
16
Authors
2
Name
Order
Citations
PageRank
Benny Godlin11839.14
Ofer Strichman2107163.61