Inference rules for proving the equivalence of recursive procedures

DOI10.1007/s00236-008-0075-2zbMath1161.68013OpenAlexW2039222548MaRDI QIDQ938300

Benny Godlin, Ofer Strichman

Publication date: 19 August 2008

Published in: Acta Informatica (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00236-008-0075-2

zbMATH Keywords

proof rulesHoare's rule for recursive procedures

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (13)

Verifying Procedural Programs via Constrained Rewriting Induction ⋮ Regression Verification for Multi-threaded Programs ⋮ Automating regression verification of pointer programs by predicate abstraction ⋮ Analysis and Transformation of Constrained Horn Clauses for Program Verification ⋮ Modular Verification of Procedure Equivalence in the Presence of Memory Allocation ⋮ Bridging arrays and ADTs in recursive proofs ⋮ Program equivalence by circular reasoning ⋮ Predicate Pairing for program verification ⋮ A language-independent proof system for full program equivalence ⋮ Inference Rules for Proving the Equivalence of Recursive Procedures ⋮ Regression verification for multi-threaded programs (with extensions to locks and dynamic thread creation) ⋮ Proving mutual termination ⋮ Abstract semantic diffing of evolving concurrent programs

Uses Software

• ACL2

Cites Work

• Unnamed Item
• Unnamed Item
• Ordinal arithmetic: Algorithms and mechanization
• On formalised computer programs
• An algorithm for reasoning about equality
• Computer Aided Verification

This page was built for publication: Inference rules for proving the equivalence of recursive procedures