Operationally-based program equivalence proofs using LCTRSs
From MaRDI portal
Publication:6052946
DOI10.1016/j.jlamp.2023.100894arXiv2001.09649OpenAlexW4384936861MaRDI QIDQ6052946
Andrei Sebastian Buruiană, Dorel Lucanu, Ştefan Ciobâcă
Publication date: 25 September 2023
Published in: Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/2001.09649
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Rewriting modulo SMT and open system analysis
- Program equivalence by circular reasoning
- A language-independent proof system for full program equivalence
- Relational separation logic
- Algorithmic games for full ground references
- Relational verification through Horn clause transformation
- A coinductive approach to proving reachability properties in logically constrained term rewriting systems
- Product programs and relational program logics
- A Theoretical Foundation for Programming Languages Aggregation
- K-Java
- Term Rewriting with Logical Constraints
- A Rewriting Logic Approach to Operational Semantics (Extended Abstract)
- A Rewriting Logic Approach to Type Inference
- Simple relational correctness proofs for static analyses and program transformations
- Automated Discovery of Simulation Between Programs
- Dependency Pairs for Rewriting with Built-In Numbers and Semantic Data Structures
- Inference Rules for Proving the Equivalence of Recursive Procedures
- Parametric polymorphism and operational equivalence
- Iris from the ground up: A modular foundation for higher-order concurrent separation logic
- Verifying Procedural Programs via Constrained Rewriting Induction
- Constrained equational deduction
- Unification Modulo Builtins
- Regression verification for multi-threaded programs (with extensions to locks and dynamic thread creation)
- Generalized rewrite theories and coherence completion
This page was built for publication: Operationally-based program equivalence proofs using LCTRSs
