Complete symbolic reachability analysis using back-and-forth narrowing

DOI10.1016/j.tcs.2006.07.008zbMath1110.68058OpenAlexW4249555655MaRDI QIDQ860885

Prasanna Thati, José Meseguer

Publication date: 9 January 2007

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2006.07.008

zbMATH Keywords

reachabilitycompletenessrewrite systemssoundnessnarrowing

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Related Items (4)

Rewriting modulo SMT and open system analysis ⋮ Twenty years of rewriting logic ⋮ A partial evaluation framework for order-sorted equational programs modulo axioms ⋮ Narrowing and Rewriting Logic: from Foundations to Applications

Uses Software

• NRL

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Lazy narrowing: strong completeness and eager variable elimination
• Programming in equational logic: Beyond strong sequentiality
• 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
• Linear unification
• Conditional narrowing modulo a set of equations
• Completeness results for basic narrowing
• The NRL Protocol Analyzer: An Overview
• A needed narrowing strategy
• On the security of public key protocols
• Functional and Logic Programming
• Algebra and Coalgebra in Computer Science
• Term Rewriting and Applications
• Rewriting Techniques and Applications
• Well-structured transition systems everywhere!

This page was built for publication: Complete symbolic reachability analysis using back-and-forth narrowing