The Maude LTL model checker

MaRDI QIDQ2851053zbMATH OpenFDO

Authors Steven Eker, José Meseguer, Ambarish Sridharanarayanan

Publication date 2 October 2013

Full work available at URL http://www.sciencedirect.com/science/article/pii/S1571066105825344

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• scientific article; zbMATH DE number 1982209
• Model checking TLR* guarantee formulas on infinite systems
• A rewriting-based model checker for the linear temporal logic of rewriting
• The Linear Temporal Logic of Rewriting Maude Model Checker
• Strategies, Model Checking and Branching-Time Properties in Maude

Cites work

• An algebraic verification of a mobile network
• An O(n log n) unidirectional distributed algorithm for extrema finding in a circle
• Conditional rewriting logic as a unified model of concurrency
• scientific article; zbMATH DE number 1670517 (Why is no real title available?)
• scientific article; zbMATH DE number 1670781 (Why is no real title available?)
• scientific article; zbMATH DE number 2089377 (Why is no real title available?)
• scientific article; zbMATH DE number 1189278 (Why is no real title available?)
• scientific article; zbMATH DE number 52331 (Why is no real title available?)
• scientific article; zbMATH DE number 1231654 (Why is no real title available?)
• scientific article; zbMATH DE number 1342254 (Why is no real title available?)
• scientific article; zbMATH DE number 1069483 (Why is no real title available?)
• scientific article; zbMATH DE number 1759609 (Why is no real title available?)
• scientific article; zbMATH DE number 1796123 (Why is no real title available?)
• scientific article; zbMATH DE number 910719 (Why is no real title available?)
• scientific article; zbMATH DE number 3227055 (Why is no real title available?)
• Myths about the mutual exclusion problem
• Plan in Maude specifying an active network programming language

Cited in

(41)

• Model checking parameterized by the semantics in Maude
• From hidden to visible: a unified framework for transforming behavioral theories into rewrite theories
• A process calculus BigrTiMo of mobile systems and its formal semantics
• A set automaton to locate all pattern matches in a term
• Strategies, model checking and branching-time properties in Maude
• Formal verification of complex business processes based on high-level Petri nets
• Simulating and model checking membrane systems using strategies in Maude
• Metalevel transformation of strategies
• Verification of the ROS NavFn planner using executable specification languages
• Egalitarian State-Transition Systems
• Proving VLRL action properties with the Maude model checker
• -calculus model checking in Maude
• A rewriting semantics for ABEL with applications to hardware/software co-design and analysis
• Verifying Reachability-Logic Properties on Rewriting-Logic Specifications
• Bringing LTL model checking to biologists
• Model checking reconfigurable Petri nets with Maude
• Verifiable abstractions for contract-oriented systems
• Model Checking LTL Formulae in RAISE with FDR
• scientific article; zbMATH DE number 1982209 (Why is no real title available?)
• An executable semantics of clock constraint specification language and its applications
• The Linear Temporal Logic of Rewriting Maude Model Checker
• Model checking of a mobile robots perpetual exploration algorithm
• Model checking strategy-controlled rewriting systems
• A language-based approach to modelling and analysis of Twitter interactions
• A rewriting-based model checker for the linear temporal logic of rewriting
• Computer Aided Verification
• Automated Technology for Verification and Analysis
• Model checking TLR* guarantee formulas on infinite systems
• Session-based concurrency in Maude: executable semantics and type checking
• QMaude: quantitative specification and verification in rewriting logic
• Strategies, Model Checking and Branching-Time Properties in Maude
• An Overview of the Maude Strategy Language and its Applications
• Maude2Lean: theorem proving for Maude specifications using Lean
• Formalization and analysis of the post-quantum signature scheme FALCON with Maude
• A rewriting logic semantics for the analysis of \textsf{P} programs
• Invariant-driven specifications in Maude
• Algebraic simulations
• Specification and analysis of the AER/NCA active network protocol suite in real-time Maude
• The rewriting logic semantics project
• Semantics and pragmatics of real-time maude
• Equational abstractions

Describes a project that uses

Uses Software

• LTL2BA
• SPIN
• Maude

This page was built for publication: The Maude LTL model checker

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