Abstract Logical Model Checking of Infinite-State Systems Using Narrowing
From MaRDI portal
Publication:2958376
DOI10.4230/LIPIcs.RTA.2013.81zbMath1356.68140OpenAlexW2294307095MaRDI 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
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 (26)
Rewriting modulo SMT and open system analysis ⋮ Executing and verifying higher-order functional-imperative programs in Maude ⋮ Optimization of rewrite theories by equational partial evaluation ⋮ Two Decades of Maude ⋮ Generic Proof Scores for Generate & Check Method in CafeOBJ ⋮ Verifying Reachability-Logic Properties on Rewriting-Logic Specifications ⋮ 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 ⋮ Verification of the ROS NavFn planner using executable specification languages ⋮ Unnamed Item ⋮ Unnamed Item ⋮ 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 ⋮ Strategies, model checking and branching-time properties in Maude ⋮ A Maude environment for CafeOBJ ⋮ All-Path Reachability Logic ⋮ Generalized rewrite theories, coherence completion, and symbolic methods ⋮ Programming and symbolic computation in Maude ⋮ Built-in Variant Generation and Unification, and Their Applications in Maude 2.7 ⋮ Generate & Check Method for Verifying Transition Systems in CafeOBJ ⋮ Equational unification and matching, and symbolic reachability analysis in Maude 3.2 (system description) ⋮ Symbolic computation in Maude: some tapas
This page was built for publication: Abstract Logical Model Checking of Infinite-State Systems Using Narrowing
