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