Matching Logic: An Alternative to Hoare/Floyd Logic

DOI10.1007/978-3-642-17796-5_9zbMath1308.68045OpenAlexW2095838677MaRDI QIDQ3067473

Wolfram Schulte, Chucky Ellison, Grigore Roşu

Publication date: 21 January 2011

Published in: Algebraic Methodology and Software Technology (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-17796-5_9

Mathematics Subject Classification ID

Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (12)

Synthesizing Loops for Program Inversion ⋮ From Jinja bytecode to term rewriting: a complexity reflecting transformation ⋮ Executing and verifying higher-order functional-imperative programs in Maude ⋮ From Rewriting Logic, to Programming Language Semantics, to Program Verification ⋮ The rewriting logic semantics project: a progress report ⋮ Twenty years of rewriting logic ⋮ A matching logic foundation for Alk ⋮ A language-independent proof system for full program equivalence ⋮ All-Path Reachability Logic ⋮ The Rewriting Logic Semantics Project: A Progress Report ⋮ Proving Reachability-Logic Formulas Incrementally ⋮ A Non-Deterministic Multiset Query Language

Uses Software

• KRAKATOA
• Why3
• Caduceus
• Maude
• ESC/Java
• K tool
• jStar
• K Prover

Cites Work

• Unnamed Item
• The Schorr-Waite graph marking algorithm
• The rewriting logic semantics project
• 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.
• Winskel is (almost) right: Towards a mechanized semantics textbook
• Forward with Hoare
• Automated Verification of the Deutsch-Schorr-Waite Tree-Traversal Algorithm
• The Logic of Bunched Implications
• Verifying properties of well-founded linked lists
• Automated Deduction – CADE-20
• Programming Languages and Systems
• An axiomatic basis for computer programming
• Tools and Algorithms for the Construction and Analysis of Systems

This page was built for publication: Matching Logic: An Alternative to Hoare/Floyd Logic