Cones and foci: A mechanical framework for protocol verification

DOI10.1007/S10703-006-0004-3MaRDI QIDQ853730zbMATH OpenOpenAlexWikidataFDO

Authors Jun Pang, Jaco van de Pol, Wan 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 algebrabranching bisimulationPVSprotocol verification

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 1956518
• Verification of a sliding window protocol in \(\mu\) CRL and PVS
• Focus points and convergent process operators: A proof strategy for protocol verification
• Formal verification of timed systems using cones and foci
• The cones and foci proof technique for timed transition systems

Cites work

• scientific article; zbMATH DE number 4110131 (Why is no real title available?)
• scientific article; zbMATH DE number 177845 (Why is no real title available?)
• scientific article; zbMATH DE number 1361141 (Why is no real title available?)
• scientific article; zbMATH DE number 1142319 (Why is no real title available?)
• scientific article; zbMATH DE number 1956518 (Why is no real title available?)
• scientific article; zbMATH DE number 1796138 (Why is no real title available?)
• scientific article; zbMATH DE number 194539 (Why is no real title available?)
• scientific article; zbMATH DE number 1361483 (Why is no real title available?)
• scientific article; zbMATH DE number 1905121 (Why is no real title available?)
• A mechanized proof environment for the convenient computations proof method
• Algebra of communicating processes with abstraction
• Algebraic Methodology and Software Technology
• Algebraic process verification.
• Branching bisimilarity is an equivalence indeed!
• Branching time and abstraction in bisimulation semantics
• Focus points and convergent process operators: A proof strategy for protocol verification
• Formal verification of a leader election protocol in process algebra
• Forward and backward simulations. I. Untimed Systems
• Isabelle/HOL. A proof assistant for higher-order logic
• Linearization in parallel pCRL
• Mechanizing UNITY in Isabelle
• On the consistency of Koomen's fair abstraction rule
• Process Algebra
• Specification of abstract data types
• Term Rewriting and All That
• The parallel composition of uniform processes with data
• The tree identify protocol of IEEE 1394 in \(\mu\)CRL
• Verification of a sliding window protocol in \(\mu\) CRL and PVS

Cited in

(11)

• scientific article; zbMATH DE number 1956518 (Why is no real title available?)
• Verification of mobile ad hoc networks: an algebraic approach
• Focus points and convergent process operators
• scientific article; zbMATH DE number 7269247 (Why is no real title available?)
• Focus points and convergent process operators: A proof strategy for protocol verification
• A linear process-algebraic format with data for probabilistic automata
• The cones and foci proof technique for timed transition systems
• Formal verification of timed systems using cones and foci
• scientific article; zbMATH DE number 1670787 (Why is no real title available?)
• Formalizing provable anonymity in Isabelle/HOL
• On the Minimisation of Acyclic Models

Describes a project that uses

Uses Software

• mCRL
• UNITY
• PVS
• Isabelle/HOL

This page was built for publication: Cones and foci: A mechanical framework for protocol verification

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