DM-check: verifying invariants of concurrent systems by deductive model checking

DOI10.1016/J.JLAMP.2025.101107MaRDI QIDQ6847672zbMATH OpenFDO

Authors Kyungmin Bae, Santiago Escobar, Raúl López-Rueda, José Meseguer, Julia Sapiña

Publication date 9 March 2026

Published in Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/J.JLAMP.2025.101107

zbMATH Keywords

invariantsmodel checkingrewriting logicinductive theorem provingconstrained patterns

Mathematics Subject Classification ID

Computer science (68-XX)

Cites work

• scientific article; zbMATH DE number 1189278 (Why is no real title available?)
• scientific article; zbMATH DE number 1142316 (Why is no real title available?)
• Abstract logical model checking of infinite-state systems using narrowing
• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• Automated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity
• Conditional rewriting logic as a unified model of concurrency
• Dependency pairs for proving termination properties of conditional term rewriting systems
• Equational unification and matching, and symbolic reachability analysis in Maude 3.2 (system description)
• Folding variant narrowing and optimal variant termination
• Generalized rewrite theories, coherence completion, and symbolic methods
• Inductive reasoning with equality predicates, contextual rewriting and variant-based simplification
• Infinite-state model checking of LTLR formulas using narrowing
• Logic-based program synthesis and transformation. 35th international symposium, LOPSTR 2025, Rende, Italy, September 9--10, 2025. Proceedings
• Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties
• Maude2Lean: theorem proving for Maude specifications using Lean
• Mechanical analysis of reliable communication in the alternating bit protocol using the Maude invariant analyzer tool
• Normal forms and normal theories in conditional rewriting
• Order-Sorted Rewriting and Congruence Closure
• Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
• Predicate abstraction of rewrite theories
• Programming and symbolic computation in Maude
• Proof scores in the OTS/CafeOBJ method.
• Proving Safety Properties of Rewrite Theories
• Symbolic Model Checking of Infinite-State Systems Using Narrowing
• Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols
• Theorem Proving Based on Proof Scores for Rewrite Theory Specifications of OTSs

Cited in

(1)

• Bounded model checking of multitask PLC ST programs with preemption using rewriting modulo SMT

This page was built for publication: DM-check: verifying invariants of concurrent systems by deductive model checking

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6847672)