Cones and foci: A mechanical framework for protocol verification

DOI10.1007/s10703-006-0004-3zbMath1103.68652WikidataQ62047493 ScholiaQ62047493MaRDI QIDQ853730

Jun Pang, Jaco van de Pol, W. J. Fokkink

Publication date: 17 November 2006

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10703-006-0004-3

zbMATH Keywords

process algebra; branching bisimulation; PVS; protocol verification

Mathematics Subject Classification ID

68Q85: Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)

Related Items

On the Minimisation of Acyclic Models

Uses Software

• Isabelle/HOL
• PVS
• UNITY
• mCRL

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Algebra of communicating processes with abstraction
• On the consistency of Koomen's fair abstraction rule
• The tree identify protocol of IEEE 1394 in \(\mu\)CRL
• Focus points and convergent process operators: A proof strategy for protocol verification
• Branching bisimilarity is an equivalence indeed!
• Formal verification of a leader election protocol in process algebra
• A mechanized proof environment for the convenient computations proof method
• Isabelle/HOL. A proof assistant for higher-order logic
• Forward and backward simulations. I. Untimed Systems
• Verification of a sliding window protocol in \(\mu\) CRL and PVS
• Process Algebra
• Branching time and abstraction in bisimulation semantics
• Term Rewriting and All That
• Algebraic Methodology and Software Technology
• Mechanizing UNITY in Isabelle
• Linearization in parallel pCRL
• The parallel composition of uniform processes with data