Generalized rewrite theories, coherence completion, and symbolic methods
From MaRDI portal
Publication:2291817
DOI10.1016/j.jlamp.2019.100483zbMath1496.68166OpenAlexW2910060813WikidataQ127348426 ScholiaQ127348426MaRDI QIDQ2291817
Publication date: 31 January 2020
Published in: Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)
Full work available at URL: http://hdl.handle.net/2142/102183
coherenceconstrained narrowinggeneralized rewrite theoriespattern predicatessymbolic invariant verification
Specification and verification (program logics, model checking, etc.) (68Q60) Grammars and rewriting systems (68Q42)
Related Items (11)
Optimization of rewrite theories by equational partial evaluation ⋮ An efficient canonical narrowing implementation with irreducibility and SMT constraints for generic symbolic protocol analysis ⋮ Symbolic Specialization of Rewriting Logic Theories with Presto ⋮ Variants and satisfiability in the infinitary unification wonderland ⋮ Strategies in conditional narrowing modulo SMT plus axioms ⋮ Optimizing Maude programs via program specialization ⋮ Unnamed Item ⋮ Guest editor's foreword ⋮ Programming and symbolic computation in Maude ⋮ Capturing constrained constructor patterns in matching logic ⋮ Symbolic computation in Maude: some tapas
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Rewriting modulo SMT and open system analysis
- State space reduction in the Maude-NRL protocol analyzer
- A generic framework for symbolic execution: a coinductive approach
- Strict coherence of conditional rewriting modulo axioms
- Normal forms and normal theories in conditional rewriting
- Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols
- Equational abstractions
- All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
- Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
- A theory of timed automata
- Equational formulae with membership constraints
- Combining symbolic constraint solvers on algebraic domains
- Equational rules for rewriting logic
- A constructor-based reachability logic for rewrite theories
- Symbolic execution based on language transformation
- A coinductive approach to proving reachability properties in logically constrained term rewriting systems
- Induction = I-axiomatization + first-order consistency.
- Implicit induction in conditional theories
- On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories
- Folding variant narrowing and optimal variant termination
- Metalevel algorithms for variant satisfiability
- Semantic foundations for generalized rewrite theories
- Equational formulas and pattern operations in initial order-sorted algebras
- Automatic Constrained Rewriting Induction towards Verifying Procedural Programs
- Term Rewriting with Logical Constraints
- Rewriting Induction + Linear Arithmetic = Decision Procedure
- Infinite-State Model Checking of LTLR Formulas Using Narrowing
- Rewriting Modulo SMT and Open System Analysis
- Verifying Reachability-Logic Properties on Rewriting-Logic Specifications
- Abstract Logical Model Checking of Infinite-State Systems Using Narrowing
- Reachability Analysis of Term Rewriting Systems with Timbuk
- Proving Safety Properties of Rewrite Theories
- Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties
- Adding nesting structure to words
- Symbolic Protocol Analysis with Disequality Constraints Modulo Equational Theories
- Bounded Model Checking of Analog and Mixed-Signal Circuits Using an SMT Solver
- Dependency Pairs for Rewriting with Built-In Numbers and Semantic Data Structures
- Rewriting Models of Boolean Programs
- Towards SMT Model Checking of Array-Based Systems
- Superposition Modulo Linear Arithmetic SUP(LA)
- Completion of a Set of Rules Modulo a Set of Equations
- Complete Sets of Reductions for Some Equational Theories
- Variant-Based Satisfiability in Initial Algebras
- Operational Termination of Conditional Rewriting with Built-in Numbers and Semantic Data Structures
- All-Path Reachability Logic
- Computer Aided Verification
- Mechanical Analysis of Reliable Communication in the Alternating Bit Protocol Using the Maude Invariant Analyzer Tool
- Symbolic Model Checking of Infinite-State Systems Using Narrowing
- Term Rewriting and Applications
- MCMT: A Model Checker Modulo Theories
- Unification Modulo Builtins
- Model Checking Software
- Perspectives of System Informatics
- Constraint-based deductive model checking
- Generalized rewrite theories and coherence completion
This page was built for publication: Generalized rewrite theories, coherence completion, and symbolic methods
