Abstract Logical Model Checking of Infinite-State Systems Using Narrowing

DOI10.4230/LIPIcs.RTA.2013.81zbMath1356.68140MaRDI QIDQ2958376

Kyungmin Bae, Santiago Escobar, José Meseguer

Publication date: 1 February 2017

Full work available at URL: https://doi.org/10.4230/lipics.rta.2013.81

model checking; narrowing; rewrite theories; infinite states

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

Unnamed Item, Unnamed Item, All-Path Reachability Logic, Generate & Check Method for Verifying Transition Systems in CafeOBJ, Model Checking TLR* Guarantee Formulas on Infinite Systems, Functional Logic Programming in Maude, Mechanical Analysis of Reliable Communication in the Alternating Bit Protocol Using the Maude Invariant Analyzer Tool, Theorem Proving Based on Proof Scores for Rewrite Theory Specifications of OTSs, Reducing non-occurrence of specified runtime errors to all-path reachability problems of constrained rewriting, Symbolic Specialization of Rewriting Logic Theories with Presto, Variants and satisfiability in the infinitary unification wonderland, Optimizing Maude programs via program specialization, Rewriting modulo SMT and open system analysis, A Maude environment for CafeOBJ, Equational unification and matching, and symbolic reachability analysis in Maude 3.2 (system description), Symbolic computation in Maude: some tapas, Strategies, model checking and branching-time properties in Maude, Generalized rewrite theories, coherence completion, and symbolic methods, Programming and symbolic computation in Maude, Executing and verifying higher-order functional-imperative programs in Maude, Optimization of rewrite theories by equational partial evaluation, Verification of the ROS NavFn planner using executable specification languages, Built-in Variant Generation and Unification, and Their Applications in Maude 2.7, Two Decades of Maude, Generic Proof Scores for Generate & Check Method in CafeOBJ, Verifying Reachability-Logic Properties on Rewriting-Logic Specifications