Symbolic Model Checking of Infinite-State Systems Using Narrowing

DOI10.1007/978-3-540-73449-9_13MaRDI QIDQ5432339zbMATH OpenOpenAlexFDO

Authors Santiago Escobar, José Meseguer

Publication date 2 January 2008

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://hdl.handle.net/2142/11292

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) 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

• Abstract logical model checking of infinite-state systems using narrowing
• Infinite-state model checking of LTLR formulas using narrowing
• Narrowing and rewriting logic: from foundations to applications
• Algebra and Coalgebra in Computer Science
• Complete symbolic reachability analysis using back-and-forth narrowing

Cited in

(37)

• State Space Reduction of Rewrite Theories Using Invisible Transitions
• Abstract logical model checking of infinite-state systems using narrowing
• Termination of Narrowing in Left-Linear Constructor Systems
• Generalized rewrite theories, coherence completion, and symbolic methods
• Twenty years of rewriting logic
• Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties
• Generic proof scores for generate \& check method in CafeOBJ
• Model checking TLR* guarantee formulas on infinite systems
• Termination of narrowing via termination of rewriting
• Generate \& check method for verifying transition systems in CafeOBJ
• Termination of narrowing revisited
• Symbolic model checking: \(10^{20}\) states and beyond
• TAGED Approximations for Temporal Properties Model-Checking
• Optimizing Maude programs via program specialization
• Modular Termination of Basic Narrowing
• Symbolic Specialization of Rewriting Logic Theories with Presto
• Infinite-state model checking of LTLR formulas using narrowing
• scientific article; zbMATH DE number 7453112 (Why is no real title available?)
• scientific article; zbMATH DE number 7455704 (Why is no real title available?)
• A rewriting-logic-with-SMT-based formal analysis and parameter synthesis framework for parametric time Petri nets
• DM-check: verifying invariants of concurrent systems by deductive model checking
• State space reduction in the Maude-NRL protocol analyzer
• Optimization of rewrite theories by equational partial evaluation
• Egalitarian State-Transition Systems
• Functional logic programming in Maude
• Rewriting modulo SMT and open system analysis
• A Finite Representation of the Narrowing Space
• Maude2Lean: theorem proving for Maude specifications using Lean
• Program equivalence by circular reasoning
• Algebra and Coalgebra in Computer Science
• Variant narrowing and equational unification
• Complete symbolic reachability analysis using back-and-forth narrowing
• Bounded model checking of multitask PLC ST programs with preemption using rewriting modulo SMT
• Two Decades of Maude
• Built-in variant generation and unification, and their applications in Maude 2.7
• scientific article; zbMATH DE number 1615252 (Why is no real title available?)
• Equational unification and matching, and symbolic reachability analysis in Maude 3.2 (system description)

Describes a project that uses

Uses Software

• Timbuk
• Maude

This page was built for publication: Symbolic Model Checking of Infinite-State Systems Using Narrowing

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