Matching Logic

DOI10.23638/LMCS-13(4:28)2017zbMath1448.03019arXiv1705.06312OpenAlexW3037272170MaRDI QIDQ4600770

Grigore Roşu

Publication date: 12 January 2018

Full work available at URL: https://arxiv.org/abs/1705.06312

zbMATH Keywords

verificationfirst-order logicrewritingprogram logic

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Grammars and rewriting systems (68Q42)

Related Items (8)

Towards a trustworthy semantics-based language framework via proof generation ⋮ A matching logic foundation for Alk ⋮ Matching µ-logic: Foundation of K framework ⋮ All-Path Reachability Logic ⋮ Matching logic explained ⋮ Many-sorted hybrid modal languages ⋮ Capturing constrained constructor patterns in matching logic ⋮ A Non-Deterministic Multiset Query Language

Uses Software

• Coq
• Isabelle/HOL
• CASL
• Why3
• z3
• CafeOBJ
• Maude
• VCC
• SLAyer
• Smallfoot
• jStar
• Python
• K Prover

This page was built for publication: Matching Logic