Variant Narrowing and Equational Unification
From MaRDI portal
Publication:5179131
DOI10.1016/j.entcs.2009.05.015zbMath1347.68194MaRDI QIDQ5179131
José Meseguer, Santiago Escobar, Ralf Sasse
Publication date: 19 March 2015
Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.entcs.2009.05.015
narrowing; cryptographic protocol analysis; symbolic reachability analysis; equational unification; finite variant property
94A60: Cryptography
68Q85: Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q42: Grammars and rewriting systems
Related Items
Variant Narrowing and Equational Unification, Optimizing Maude programs via program specialization, State space reduction in the Maude-NRL protocol analyzer, A generic framework for symbolic execution: a coinductive approach, An integrated framework for the diagnosis and correction of rule-based programs, Symbolic execution based on language transformation, Capturing constrained constructor patterns in matching logic, A partial evaluation framework for order-sorted equational programs modulo axioms, Optimization of rewrite theories by equational partial evaluation, On First-Order Model-Based Reasoning, Model Checking Security Protocols, Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties, Effectively Checking the Finite Variant Property, Termination Modulo Combinations of Equational Theories
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- A rewriting-based inference system for the NRL protocol analyzer and its meta-logical properties
- Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols
- Conditional rewriting logic as a unified model of concurrency
- Equational rules for rewriting logic
- Matching, unification and complexity
- Effectively Checking the Finite Variant Property
- Complete Sets of Reductions for Some Equational Theories
- Lazy narrowing with simplification
- Variant Narrowing and Equational Unification
- Symbolic Model Checking of Infinite-State Systems Using Narrowing
- Term Rewriting and Applications
- Term Rewriting and Applications