Executing and verifying higher-order functional-imperative programs in Maude
From MaRDI portal
Publication:2409629
DOI10.1016/j.jlamp.2017.09.002zbMath1372.68056OpenAlexW2759708576MaRDI QIDQ2409629
Publication date: 13 October 2017
Published in: Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)
Full work available at URL: https://hal.inria.fr/hal-01586341/file/wrla-jlamp-R2.pdf
Uses Software
Cites Work
- Rewriting modulo SMT and open system analysis
- Program equivalence by circular reasoning
- A generic framework for symbolic execution: a coinductive approach
- A language-independent proof system for full program equivalence
- Language definitions as rewrite theories
- All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
- Symbolic execution based on language transformation
- Proving Reachability-Logic Formulas Incrementally
- TRACER: A Symbolic Execution Tool for Verification
- Rewriting Modulo SMT and Open System Analysis
- Abstract Logical Model Checking of Infinite-State Systems Using Narrowing
- Matching Logic: An Alternative to Hoare/Floyd Logic
- Structural Analysis of Narratives with the Coq Proof Assistant
- Towards a Unified Theory of Operational and Axiomatic Semantics
- A Hoare Logic for the State Monad
- Inference Rules for Proving the Equivalence of Recursive Procedures
- Symbolic execution and program testing
- All-Path Reachability Logic
- One-Path Reachability Logic
- Matching Logic - Extended Abstract (Invited Talk)
- Computer Aided Verification
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: Executing and verifying higher-order functional-imperative programs in Maude