Term Rewriting and Applications

DOI10.1007/b135673zbMath1078.68059OpenAlexW2504734884MaRDI QIDQ5703857

Stéphanie Delaune, Hubert Comon-Lundh

Publication date: 11 November 2005

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/b135673

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Related Items (42)

Non-disjoint combined unification and closure by equational paramodulation ⋮ Model Checking Security Protocols ⋮ Symbolic Protocol Analysis with Disequality Constraints Modulo Equational Theories ⋮ Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties ⋮ Optimization of rewrite theories by equational partial evaluation ⋮ Metalevel algorithms for variant satisfiability ⋮ Alice and Bob Meet Equational Theories ⋮ Two Decades of Maude ⋮ Emerging Issues and Trends in Formal Methods in Cryptographic Protocol Analysis: Twelve Years Later ⋮ Twenty years of rewriting logic ⋮ An efficient canonical narrowing implementation with irreducibility and SMT constraints for generic symbolic protocol analysis ⋮ Unnamed Item ⋮ Variants and satisfiability in the infinitary unification wonderland ⋮ Variant-based equational anti-unification ⋮ Optimizing Maude programs via program specialization ⋮ Effectively Checking the Finite Variant Property ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Challenges in the Automated Verification of Security Protocols ⋮ Computing knowledge in equational extensions of subterm convergent theories ⋮ Beyond Subterm-Convergent Equational Theories in Automated Verification of Stateful Protocols ⋮ A survey of symbolic methods for establishing equivalence-based properties in cryptographic protocols ⋮ Symbolic protocol analysis for monoidal equational theories ⋮ Hierarchical combination of intruder theories ⋮ Reducing protocol analysis with XOR to the XOR-free case in the Horn theory based approach ⋮ Termination of narrowing via termination of rewriting ⋮ Variant Narrowing and Equational Unification ⋮ A procedure for deciding symbolic equivalence between sets of constraint systems ⋮ Variant-Based Satisfiability in Initial Algebras ⋮ Generalized rewrite theories, coherence completion, and symbolic methods ⋮ Programming and symbolic computation in Maude ⋮ A partial evaluation framework for order-sorted equational programs modulo axioms ⋮ Ground confluence of order-sorted conditional specifications modulo axioms ⋮ Automated Verification of Equivalence Properties of Cryptographic Protocols ⋮ Built-in Variant Generation and Unification, and Their Applications in Maude 2.7 ⋮ Combining proverif and automated theorem provers for security protocol verification ⋮ Protocol Security and Algebraic Properties: Decision Results for a Bounded Number of Sessions ⋮ Metalevel Algorithms for Variant Satisfiability ⋮ Termination Modulo Combinations of Equational Theories ⋮ Equational unification and matching, and symbolic reachability analysis in Maude 3.2 (system description) ⋮ Symbolic computation in Maude: some tapas ⋮ Terminating non-disjoint combined unification

This page was built for publication: Term Rewriting and Applications