Cones and foci: A mechanical framework for protocol verification

W.J. Fokkink, J. Pang, J.C. van de Pol

Research output: Contribution to JournalArticleAcademicpeer-review


We define a cones and foci proof method, which rephrases the question whether two system specifications are branching bisimilar in terms of proof obligations on relations between data objects. Compared to the original cones and foci method from Groote and Springintveld, our method is more generally applicable, because it does not require a preprocessing step to eliminate τ-loops. We prove soundness of our approach and present a set of rules to prove the reachability of focus points. Our method has been formalized and proved correct using PVS. Thus we have established a framework for mechanical protocol verification. We apply this framework to the Concurrent Alternating Bit Protocol.
Original languageEnglish
Pages (from-to)1-31
JournalFormal Methods in System Design
Issue number1
Publication statusPublished - 2006

Bibliographical note



Dive into the research topics of 'Cones and foci: A mechanical framework for protocol verification'. Together they form a unique fingerprint.

Cite this