Cited in
(66)- Optimization of rewrite theories by equational partial evaluation
- Tree automata for detecting attacks on protocols with algebraic cryptographic primitives
- Combining proverif and automated theorem provers for security protocol verification
- A reduced semantics for deciding trace equivalence
- Variant narrowing and equational unification
- Built-in variant generation and unification, and their applications in Maude 2.7
- José Meseguer: scientist and friend extraordinaire
- Programming and symbolic computation in Maude
- Automated verification of equivalence properties of cryptographic protocols
- Order-sorted equational unification revisited
- A formalisation of nominal \(\alpha\)-equivalence with A, C, and AC function symbols
- Two Decades of Maude
- Sentence-Normalized Conditional Narrowing Modulo in Rewriting Logic and Maude
- Sentence-normalized conditional narrowing modulo in rewriting logic and Maude
- Model Checking Security Protocols
- Beyond Subterm-Convergent Equational Theories in Automated Verification of Stateful Protocols
- Intruder deduction problem for locally stable theories with normal forms and inverses
- YAPA
- AVISPA
- ECCE
- FAST
- Maude
- ProVerif
- Timbuk
- 2OBJ
- PMaude
- PAGODA
- OFMC
- SATMC
- scyther
- HI-maude
- K-Maude
- MFE
- ITP
- MTT
- CARIBOO
- Anima
- InvA
- NRL
- vlogsl
- FreshML
- Akiss
- Apte
- SymPLFIED
- TAMARIN
- margrave
- Z3str2
- ABETS
- ACUOS2
- KOOL
- CPSA
- Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties
- Bounded ACh unification
- GLINTS
- Efficient general unification for XOR with homomorphism
- A formalisation of nominal \(\alpha\)-equivalence with A and AC function symbols
- Generalized rewrite theories, coherence completion, and symbolic methods
- Symbolic Protocol Analysis with Disequality Constraints Modulo Equational Theories
- Symbolic computation in Maude: some tapas
- scientific article; zbMATH DE number 7453112 (Why is no real title available?)
- scientific article; zbMATH DE number 7455704 (Why is no real title available?)
- Terminating non-disjoint combined unification
- Computing knowledge in equational extensions of subterm convergent theories
- Equational unification and matching, and symbolic reachability analysis in Maude 3.2 (system description)
- Twenty years of rewriting logic
- Efficient general AGH-unification
This page was built for software: Maude-NPA
