Inference Rules for Proving the Equivalence of Recursive Procedures

DOI10.1007/978-3-642-13754-9_8zbMath1288.68042OpenAlexW2406820219MaRDI QIDQ3587255

Benny Godlin, Ofer Strichman

Publication date: 7 September 2010

Published in: Time for Verification (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-13754-9_8

Mathematics Subject Classification ID

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

Related Items (5)

Verifying Procedural Programs via Constrained Rewriting Induction ⋮ Executing and verifying higher-order functional-imperative programs in Maude ⋮ Operationally-based program equivalence proofs using LCTRSs ⋮ A language-independent proof system for full program equivalence ⋮ Certified abstract cost analysis

Uses Software

• ACL2

Cites Work

• Ordinal arithmetic: Algorithms and mechanization
• Inference rules for proving the equivalence of recursive procedures
• On formalised computer programs
• An axiomatic basis for computer programming
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Inference Rules for Proving the Equivalence of Recursive Procedures