Program equivalence by circular reasoning

DOI10.1007/s00165-014-0319-6zbMath1319.68060OpenAlexW1964110138MaRDI QIDQ493521

Dorel Lucanu, Vlad Rusu

Publication date: 3 September 2015

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00165-014-0319-6

zbMATH Keywords

proof systemprogram equivalencelanguage independence

Mathematics Subject Classification ID

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

Related Items (4)

Executing and verifying higher-order functional-imperative programs in Maude ⋮ Operationally-based program equivalence proofs using LCTRSs ⋮ Program equivalence by circular reasoning ⋮ A language-independent proof system for full program equivalence

Uses Software

• z3
• CIRC
• Maude
• SymDiff
• Featherweight Java
• coFJ
• K Prover

Cites Work

• Unnamed Item
• Unnamed Item
• Program equivalence by circular reasoning
• A generic framework for symbolic execution: a coinductive approach
• A language-independent proof system for full program equivalence
• Inference rules for proving the equivalence of recursive procedures
• An overview of the K semantic framework
• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• Circular Coinduction: A Proof Theoretical Foundation
• Regression Verification for Multi-threaded Programs
• A Decision Procedure for Bisimilarity of Generalized Regular Expressions
• From Hoare Logic to Matching Logic Reachability
• A logic for information flow in object-oriented programs
• Automatic Validation of Transformation Rules for Java Verification Against a Rewriting Semantics
• Co-Logic Programming: Extending Logic Programming with Coinduction
• Symbolic Model Checking of Infinite-State Systems Using Narrowing
• Computer Aided Verification

This page was built for publication: Program equivalence by circular reasoning