Generalized rewrite theories, coherence completion, and symbolic methods
From MaRDI portal
Publication:2291817
DOI10.1016/J.JLAMP.2019.100483zbMATH Open1496.68166OpenAlexW2910060813WikidataQ127348426 ScholiaQ127348426MaRDI QIDQ2291817FDOQ2291817
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
Grammars and rewriting systems (68Q42) Specification and verification (program logics, model checking, etc.) (68Q60)
Cites Work
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- 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
- Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
- Adding nesting structure to words
- Complete Sets of Reductions for Some Equational Theories
- MCMT: A Model Checker Modulo Theories
- Combining symbolic constraint solvers on algebraic domains
- Equational rules for rewriting logic
- Semantic foundations for generalized rewrite theories
- 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)
- Operational Termination of Conditional Rewriting with Built-in Numbers and Semantic Data Structures
- Perspectives of System Informatics
- 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
- Implicit induction in conditional theories
- 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
- On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories
- Folding variant narrowing and optimal variant termination
- Strict coherence of conditional rewriting modulo axioms
- Equational formulae with membership constraints
- Variant-Based Satisfiability in Initial Algebras
- Induction = I-axiomatization + first-order consistency.
- Equational formulas and pattern operations in initial order-sorted algebras
- Model Checking Software
- 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 (20)
- 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
- 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
- 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)
