Generalized rewrite theories, coherence completion, and symbolic methods
From MaRDI portal
Publication:2291817
DOI10.1016/J.JLAMP.2019.100483zbMATH Open1496.68166OpenAlexW2910060813WikidataQ127348426 ScholiaQ127348426MaRDI QIDQ2291817FDOQ2291817
Authors: Yanyan Li 
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
Recommendations
coherenceconstrained narrowinggeneralized rewrite theoriespattern predicatessymbolic invariant verification
Grammars and rewriting systems (68Q42) Specification and verification (program logics, model checking, etc.) (68Q60)
Cites Work
- All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
- State space reduction in the Maude-NRL protocol analyzer
- Computer Aided Verification
- A theory of timed automata
- Title not available (Why is that?)
- Title not available (Why is that?)
- Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
- Adding nesting structure to words
- Title not available (Why is that?)
- Complete Sets of Reductions for Some Equational Theories
- MCMT: a model checker modulo theories
- Title not available (Why is that?)
- Title not available (Why is that?)
- Combining symbolic constraint solvers on algebraic domains
- Equational rules for rewriting logic
- Semantic foundations for generalized rewrite theories
- Title not available (Why is that?)
- Title not available (Why is that?)
- Automatic constrained rewriting induction towards verifying procedural programs
- Term Rewriting with Logical Constraints
- Rewriting Induction + Linear Arithmetic = Decision Procedure
- Rewriting modulo SMT and open system analysis
- Abstract logical model checking of infinite-state systems using narrowing
- Rewriting modulo SMT and open system analysis
- 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
- Towards SMT Model Checking of Array-Based Systems
- Superposition modulo linear arithmetic SUP(LA)
- Title not available (Why is that?)
- Operational termination of conditional rewriting with built-in numbers and semantic data structures
- A logical reconstruction of reachability
- Constraint-based deductive model checking
- Normal forms and normal theories in conditional rewriting
- Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols
- Title not available (Why is that?)
- Implicit induction in conditional theories
- Title not available (Why is that?)
- Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties
- Symbolic Model Checking of Infinite-State Systems Using Narrowing
- Equational abstractions
- Reachability analysis of term rewriting systems with Timbuk
- A generic framework for symbolic execution: a coinductive approach
- Verifying Reachability-Logic Properties on Rewriting-Logic Specifications
- All-path reachability logic
- Term Rewriting and Applications
- Completion of a Set of Rules Modulo a Set of Equations
- A coinductive approach to proving reachability properties in logically constrained term rewriting systems
- Title not available (Why is that?)
- Title not available (Why is that?)
- On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories
- Folding variant narrowing and optimal variant termination
- Title not available (Why is that?)
- Strict coherence of conditional rewriting modulo axioms
- Equational formulae with membership constraints
- Title not available (Why is that?)
- Variant-Based Satisfiability in Initial Algebras
- Induction = I-axiomatization + first-order consistency.
- Title not available (Why is that?)
- Equational formulas and pattern operations in initial order-sorted algebras
- Model Checking Software
- Title not available (Why is that?)
- Proving Safety Properties of Rewrite Theories
- Infinite-state model checking of LTLR formulas using narrowing
- A constructor-based reachability logic for rewrite theories
- Symbolic execution based on language transformation
- Metalevel algorithms for variant satisfiability
- Symbolic Protocol Analysis with Disequality Constraints Modulo Equational Theories
- Rewriting Models of Boolean Programs
- Mechanical analysis of reliable communication in the alternating bit protocol using the Maude invariant analyzer tool
- Unification Modulo Builtins
- Generalized rewrite theories and coherence completion
Cited In (22)
- Symbolic computation in Maude: some tapas
- Building correct-by-construction systems with formal patterns
- Canonized Rewriting and Ground AC Completion Modulo Shostak Theories
- Rewriting in Gray categories with applications to coherence
- Optimizing Maude programs via program specialization
- Strategies in conditional narrowing modulo SMT plus axioms
- Term Rewriting and Applications
- Generalized rewrite theories and coherence completion
- Symbolic Specialization of Rewriting Logic Theories with Presto
- Title not available (Why is that?)
- A rewriting-logic-with-SMT-based formal analysis and parameter synthesis framework for parametric time Petri nets
- Canonized rewriting and ground AC completion modulo Shostak theories: design and implementation
- An efficient canonical narrowing implementation with irreducibility and SMT constraints for generic symbolic protocol analysis
- Programming and symbolic computation in Maude
- Guest editor's foreword
- Optimization of rewrite theories by equational partial evaluation
- Canonical Narrowing with Irreducibility and SMT Constraints as a Generic Symbolic Protocol Analysis Method
- Maude2Lean: theorem proving for Maude specifications using Lean
- Variants and satisfiability in the infinitary unification wonderland
- Symbolic analysis and parameter synthesis for time Petri nets using Maude and SMT solving
- A Maude coherence checker tool for conditional order-sorted rewrite theories
- Capturing constrained constructor patterns in matching logic
Uses Software
This page was built for publication: Generalized rewrite theories, coherence completion, and symbolic methods
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2291817)
