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

DOI10.1016/S1567-8326(01)00010-8zbMATH Open1015.68175OpenAlexW2019702515WikidataQ127120454 ScholiaQ127120454MaRDI QIDQ1349249FDOQ1349249

Authors: Jan Friso Groote, J. Springintveld 

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

Recommendations

• Cones and foci: A mechanical framework for protocol verification
• Focus points and convergent process operators
• Algebraic process verification.
• scientific article; zbMATH DE number 3958712
• Formalizing process algebraic verifications in the calculus of constructions

zbMATH Keywords

algebraic protocol verificationconcurrent alternating bit protocol

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (12)

• Distributed consensus, revisited
• Title not available (Why is that?)
• On process equivalence = equation solving in CCS
• Title not available (Why is that?)
• Verification of mobile ad hoc networks: an algebraic approach
• Linearization in parallel pCRL
• Focus points and convergent process operators
• Cones and foci: A mechanical framework for protocol verification
• Title not available (Why is that?)
• A linear process-algebraic format with data for probabilistic automata
• Algebraic process verification.
• A compositional protocol verification using relativized bisimulation

Uses Software

• Coq
• UNITY

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

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