Variant narrowing and equational unification

DOI10.1016/J.ENTCS.2009.05.015MaRDI QIDQ5179131zbMATH OpenOpenAlexFDO

Authors Santiago Escobar, José Meseguer, 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

zbMATH Keywords

cryptographic protocol analysisequational unificationfinite variant propertynarrowingsymbolic reachability analysis

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Cryptography (94A60)

Recommendations

• Folding variant narrowing and optimal variant termination
• Conditional narrowing modulo a set of equations
• S-narrowing for constructor systems
• Folding Variant Narrowing and Optimal Variant Termination
• Narrowing and rewriting logic: from foundations to applications

Cites work

• A rewriting-based inference system for the NRL protocol analyzer and its meta-logical properties
• Complete Sets of Reductions for Some Equational Theories
• Conditional rewriting logic as a unified model of concurrency
• Effectively Checking the Finite Variant Property
• Equational rules for rewriting logic
• scientific article; zbMATH DE number 3817070 (Why is no real title available?)
• scientific article; zbMATH DE number 1189278 (Why is no real title available?)
• scientific article; zbMATH DE number 3688776 (Why is no real title available?)
• scientific article; zbMATH DE number 1142316 (Why is no real title available?)
• scientific article; zbMATH DE number 2044516 (Why is no real title available?)
• scientific article; zbMATH DE number 1889386 (Why is no real title available?)
• Lazy narrowing with simplification
• Matching, unification and complexity
• Symbolic Model Checking of Infinite-State Systems Using Narrowing
• Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols
• Term Rewriting and Applications
• Term Rewriting and Applications
• Unification theory
• Variant narrowing and equational unification

Cited in

(29)

• Narrowing based procedures for equational disunification
• Conditional narrowing modulo a set of equations
• Symbolic execution based on language transformation
• Folding variant narrowing and optimal variant termination
• Capturing constrained constructor patterns in matching logic
• Reviving basic narrowing modulo
• A partial evaluation framework for order-sorted equational programs modulo axioms
• Optimization of rewrite theories by equational partial evaluation
• Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols
• Narrowing and rewriting logic: from foundations to applications
• S-narrowing for constructor systems
• 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
• Variant Construction from Theoretical Foundation to Applications
• State space reduction in the Maude-NRL protocol analyzer
• scientific article; zbMATH DE number 7453112 (Why is no real title available?)
• scientific article; zbMATH DE number 7455704 (Why is no real title available?)
• A generic framework for symbolic execution: a coinductive approach
• Variant narrowing and equational unification
• Variants, unification, narrowing, and symbolic reachability in Maude 2.6
• An integrated framework for the diagnosis and correction of rule-based programs
• Variant-based equational anti-unification
• Optimizing Maude programs via program specialization
• Nominal equational rewriting and narrowing
• Nominal equational narrowing: rewriting for unification in languages with binders
• Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols

Describes a project that uses

Uses Software

• Maude-NPA

This page was built for publication: Variant narrowing and equational unification

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5179131)