Symbolic Model Checking of Infinite-State Systems Using Narrowing
From MaRDI portal
Publication:5432339
DOI10.1007/978-3-540-73449-9_13zbMath1203.68097OpenAlexW2146005157MaRDI QIDQ5432339
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
Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Grammars and rewriting systems (68Q42)
Related Items (25)
A Finite Representation of the Narrowing Space ⋮ Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties ⋮ Optimization of rewrite theories by equational partial evaluation ⋮ Two Decades of Maude ⋮ Generic Proof Scores for Generate & Check Method in CafeOBJ ⋮ Twenty years of rewriting logic ⋮ Symbolic Specialization of Rewriting Logic Theories with Presto ⋮ Optimizing Maude programs via program specialization ⋮ Modular Termination of Basic Narrowing ⋮ Unnamed Item ⋮ Unnamed Item ⋮ State space reduction in the Maude-NRL protocol analyzer ⋮ Program equivalence by circular reasoning ⋮ Model Checking TLR* Guarantee Formulas on Infinite Systems ⋮ Functional Logic Programming in Maude ⋮ Termination of narrowing via termination of rewriting ⋮ Variant Narrowing and Equational Unification ⋮ Termination of Narrowing in Left-Linear Constructor Systems ⋮ Generalized rewrite theories, coherence completion, and symbolic methods ⋮ Built-in Variant Generation and Unification, and Their Applications in Maude 2.7 ⋮ TAGED Approximations for Temporal Properties Model-Checking ⋮ Egalitarian State-Transition Systems ⋮ Termination of narrowing revisited ⋮ Generate & Check Method for Verifying Transition Systems in CafeOBJ ⋮ Equational unification and matching, and symbolic reachability analysis in Maude 3.2 (system description)
Uses Software
This page was built for publication: Symbolic Model Checking of Infinite-State Systems Using Narrowing
