Proof-checking protocols using bisimulations

DOI10.1007/3-540-48320-9_36MaRDI QIDQ4270079zbMATH OpenFDO

Authors Christine Röckl, Javier Esparza

Publication date 19 July 2000

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-48320-9_36

zbMATH Keywords

Isabelle/HOL theorem prover

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 2102719
• A completeness proof for bisimulation in the pi-calculus using Isabelle
• scientific article; zbMATH DE number 2185678
• Tools and Algorithms for the Construction and Analysis of Systems
• Incremental pattern-based coinduction for process algebra and its Isabelle formalization

Cited in

(10)

• Program constructions that are safe for bisimulation
• Bisimulations for verifying strategic abilities with an application to the ThreeBallot voting protocol
• Formalising Observer Theory for Environment-Sensitive Bisimulation
• Incremental pattern-based coinduction for process algebra and its Isabelle formalization
• scientific article; zbMATH DE number 4022620 (Why is no real title available?)
• scientific article; zbMATH DE number 2038740 (Why is no real title available?)
• scientific article; zbMATH DE number 2102719 (Why is no real title available?)
• Tools and Algorithms for the Construction and Analysis of Systems
• Cones and foci: A mechanical framework for protocol verification
• Using probabilistic Kleene algebra pKA for protocol verification

Describes a project that uses

Uses Software

• Isabelle/HOL

This page was built for publication: Proof-checking protocols using bisimulations

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