Equational unification and matching, and symbolic reachability analysis in Maude 3.2 (system description)
From MaRDI portal
Publication:2104541
Cites work
- scientific article; zbMATH DE number 1189278 (Why is no real title available?)
- scientific article; zbMATH DE number 1231543 (Why is no real title available?)
- scientific article; zbMATH DE number 1142316 (Why is no real title available?)
- scientific article; zbMATH DE number 1881074 (Why is no real title available?)
- scientific article; zbMATH DE number 3413831 (Why is no real title available?)
- A Machine-Oriented Logic Based on the Resolution Principle
- A constructor-based reachability logic for rewrite theories
- A mechanical solution of Schubert's steamroller by many-sorted resolution
- A partial evaluation framework for order-sorted equational programs modulo axioms
- Abstract logical model checking of infinite-state systems using narrowing
- All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
- Automated verification of equivalence properties of cryptographic protocols
- Built-in variant generation and unification, and their applications in Maude 2.7
- Complete Sets of Reductions for Some Equational Theories
- Folding variant narrowing and optimal variant termination
- Ground confluence of order-sorted conditional specifications modulo axioms
- Matching, unification and complexity
- Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties
- Metalevel algorithms for variant satisfiability
- Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
- Paramodulation-based theorem proving
- Programming and symbolic computation in Maude
- Proving Safety Properties of Rewrite Theories
- Pure type systems in rewriting logic: specifying typed higher-order languages in a first-order logical framework
- Reflective metalogical frameworks
- Semantics and pragmatics of real-time maude
- Strict coherence of conditional rewriting modulo axioms
- Symbolic Model Checking of Infinite-State Systems Using Narrowing
- Symbolic computation in Maude: some tapas
- Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols
- Symbolic reasoning methods in rewriting logic and Maude
- Term Rewriting and Applications
- The 2D dependency pair framework for conditional rewrite systems. I: Definition and basic processors
- The 2D dependency pair framework for conditional rewrite systems. II: Advanced processors and implementation techniques
- Variant-Based Satisfiability in Initial Algebras
- Z3str2: an efficient solver for strings, regular expressions, and length constraints
- \({\mathsf{ACUOS}}^\mathbf{2}\): a high-performance system for modular ACU generalization with subtyping and inheritance
Cited in
(5)- Building correct-by-construction systems with formal patterns
- Maude
- Verification of the ROS NavFn planner using executable specification languages
- Variants and satisfiability in the infinitary unification wonderland
- A rewriting logic approach to specification, proof-search, and meta-proofs in sequent systems
This page was built for publication: Equational unification and matching, and symbolic reachability analysis in Maude 3.2 (system description)
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2104541)
