Focus points and convergent process operators: A proof strategy for protocol verification

DOI10.1016/S1567-8326(01)00010-8zbMath1015.68175OpenAlexW2019702515WikidataQ127120454 ScholiaQ127120454MaRDI QIDQ1349249

Jan Springintveld, Jan Friso Groote

Publication date: 21 May 2002

Published in: The Journal of Logic and Algebraic Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s1567-8326(01)00010-8

zbMATH Keywords

algebraic protocol verificationconcurrent alternating bit protocol

Mathematics Subject Classification ID

Related Items (7)

On process equivalence = equation solving in CCS ⋮ Cones and foci: A mechanical framework for protocol verification ⋮ Distributed consensus, revisited ⋮ Verification of mobile ad hoc networks: an algebraic approach ⋮ Linearization in parallel pCRL ⋮ Unnamed Item ⋮ A linear process-algebraic format with data for probabilistic automata

Uses Software

• Coq
• UNITY

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• The tree identify protocol of IEEE 1394 in \(\mu\)CRL
• A compositional protocol verification using relativized bisimulation
• Formal verification of a leader election protocol in process algebra
• The cones and foci proof technique for timed transition systems
• Forward and backward simulations. I. Untimed Systems
• A computer checked algebraic verification of a distributed summation algorithm
• Process Algebra
• Applications of Process Algebra
• Branching time and abstraction in bisimulation semantics
• Linearization in parallel pCRL

This page was built for publication: Focus points and convergent process operators: A proof strategy for protocol verification