Generalized rewrite theories, coherence completion, and symbolic methods
From MaRDI portal
(Redirected from Publication:2291817)
Recommendations
Cites work
- scientific article; zbMATH DE number 1617315 (Why is no real title available?)
- scientific article; zbMATH DE number 1670791 (Why is no real title available?)
- scientific article; zbMATH DE number 1688812 (Why is no real title available?)
- scientific article; zbMATH DE number 4130339 (Why is no real title available?)
- scientific article; zbMATH DE number 3888893 (Why is no real title available?)
- scientific article; zbMATH DE number 3911679 (Why is no real title available?)
- scientific article; zbMATH DE number 1189278 (Why is no real title available?)
- scientific article; zbMATH DE number 3703962 (Why is no real title available?)
- scientific article; zbMATH DE number 177848 (Why is no real title available?)
- scientific article; zbMATH DE number 3549200 (Why is no real title available?)
- scientific article; zbMATH DE number 1142316 (Why is no real title available?)
- scientific article; zbMATH DE number 2043549 (Why is no real title available?)
- scientific article; zbMATH DE number 1754582 (Why is no real title available?)
- scientific article; zbMATH DE number 3249766 (Why is no real title available?)
- scientific article; zbMATH DE number 3367095 (Why is no real title available?)
- scientific article; zbMATH DE number 3387326 (Why is no real title available?)
- A coinductive approach to proving reachability properties in logically constrained term rewriting systems
- A constructor-based reachability logic for rewrite theories
- A generic framework for symbolic execution: a coinductive approach
- A logical reconstruction of reachability
- A theory of timed automata
- Abstract logical model checking of infinite-state systems using narrowing
- Adding nesting structure to words
- All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
- Automatic constrained rewriting induction towards verifying procedural programs
- Bounded Model Checking of Analog and Mixed-Signal Circuits Using an SMT Solver
- Combining symbolic constraint solvers on algebraic domains
- Complete Sets of Reductions for Some Equational Theories
- Completion of a Set of Rules Modulo a Set of Equations
- Computer Aided Verification
- Constraint-based deductive model checking
- Dependency Pairs for Rewriting with Built-In Numbers and Semantic Data Structures
- Equational abstractions
- Equational formulae with membership constraints
- Equational formulas and pattern operations in initial order-sorted algebras
- Equational rules for rewriting logic
- Folding variant narrowing and optimal variant termination
- Generalized rewrite theories and coherence completion
- Implicit induction in conditional theories
- Induction = I-axiomatization + first-order consistency.
- Infinite-state model checking of LTLR formulas using narrowing
- MCMT: a model checker modulo theories
- Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties
- Mechanical analysis of reliable communication in the alternating bit protocol using the Maude invariant analyzer tool
- Metalevel algorithms for variant satisfiability
- Model Checking Software
- Normal forms and normal theories in conditional rewriting
- On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories
- Operational termination of conditional rewriting with built-in numbers and semantic data structures
- Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
- Proving Safety Properties of Rewrite Theories
- Reachability analysis of term rewriting systems with Timbuk
- Rewriting Induction + Linear Arithmetic = Decision Procedure
- Rewriting Models of Boolean Programs
- Rewriting modulo SMT and open system analysis
- Rewriting modulo SMT and open system analysis
- Semantic foundations for generalized rewrite theories
- State space reduction in the Maude-NRL protocol analyzer
- Strict coherence of conditional rewriting modulo axioms
- Superposition modulo linear arithmetic SUP(LA)
- Symbolic Model Checking of Infinite-State Systems Using Narrowing
- Symbolic Protocol Analysis with Disequality Constraints Modulo Equational Theories
- Symbolic execution based on language transformation
- Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols
- Term Rewriting and Applications
- Term Rewriting with Logical Constraints
- Towards SMT Model Checking of Array-Based Systems
- Unification Modulo Builtins
- Variant-Based Satisfiability in Initial Algebras
- Verifying Reachability-Logic Properties on Rewriting-Logic Specifications
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
- scientific article; zbMATH DE number 7455704 (Why is no real title available?)
- 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
- Programming and symbolic computation in Maude
- An efficient canonical narrowing implementation with irreducibility and SMT constraints for generic symbolic protocol analysis
- Optimization of rewrite theories by equational partial evaluation
- Guest editor's foreword
- 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
Describes a project that uses
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)
