Executing and verifying higher-order functional-imperative programs in Maude

DOI10.1016/j.jlamp.2017.09.002zbMath1372.68056OpenAlexW2759708576MaRDI QIDQ2409629

Vlad Rusu, Andrei Arusoaie

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

zbMATH Keywords

higher-order functionMaudereachability logicstate monad

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Logic in computer science (03B70)

Uses Software

• Coq
• CUTE
• KLEE
• Maude
• DART
• Pex
• TRACER
• STP

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