A language-independent proof system for full program equivalence
From MaRDI portal
Publication:510898
DOI10.1007/s00165-016-0361-7zbMath1355.68051OpenAlexW2315369658MaRDI QIDQ510898
Vlad Rusu, Dorel Lucanu, Ştefan Ciobâcă, Grigore Roşu
Publication date: 14 February 2017
Published in: Formal Aspects of Computing (Search for Journal in Brave)
Full work available at URL: https://hal.inria.fr/hal-01245528/file/icfem-postproceedings-final-version.pdf
full equivalenceprogramming language semanticsprogram equivalencematching logicprogramming language aggregation
Logic in computer science (03B70) Applications of universal algebra in computer science (08A70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items
Executing and verifying higher-order functional-imperative programs in Maude, Operationally-based program equivalence proofs using LCTRSs, Program equivalence by circular reasoning
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Program equivalence by circular reasoning
- A generic framework for symbolic execution: a coinductive approach
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Inference rules for proving the equivalence of recursive procedures
- A rewriting logic approach to operational semantics
- An Institutional Foundation for the $$\mathbb {K}$$K Semantic Framework
- A Theoretical Foundation for Programming Languages Aggregation
- K-Java
- Regression Verification for Multi-threaded Programs
- Biorthogonality, step-indexing and compiler correctness
- The marriage of bisimulations and Kripke logical relations
- Matching Logic: An Alternative to Hoare/Floyd Logic
- Introduction to Bisimulation and Coinduction
- Towards a Unified Theory of Operational and Axiomatic Semantics
- Simple relational correctness proofs for static analyses and program transformations
- Logical Bisimulations and Functional Languages
- Inference Rules for Proving the Equivalence of Recursive Procedures
- From Hoare Logic to Matching Logic Reachability
- Don't Try to Solve These Problems
- Towards Modularly Comparing Programs Using Automated Theorem Provers
- All-Path Reachability Logic
- State-dependent representation independence
- One-Path Reachability Logic
- Matching Logic - Extended Abstract (Invited Talk)
- Automated Reasoning
- A kripke logical relation between ML and assembly
- Equality of streams is a Π0 over 2-complete problem
- An axiomatic basis for computer programming
- Computer Aided Verification
