




Publications  ProofChecking Protocols Using Bisimulations





Reference:
C. Röckl and J. Esparza. Proofchecking protocols using bisimulations. In J. C. M. Baeten and S. Mauw, editors, Proc. of CONCUR'99, number 1664 in Lecture Notes in Computer Science, pages 525–540. SpringerVerlag, 1999.
Abstract:
Observation equivalence is of particular interest to the verification of concurrent systems, as it is compositional, detects deadlocks, and possesses a welldeveloped theory. We examine the mechanization of proofs by exhibiting bisimulation relations. As examples we have chosen infinitestate, as well as parameterized systems, that cannot be treated by fully automatic tools based on exploring the complete state space. The description of the systems is given by a transition semantics based on valuepassing processes, though automata models, for instance, would be equally applicable. For the mechanization, we use the interactive theorem prover Isabelle/HOL, as it enables the user to apply inductive definitions and proofs, and provides powerful builtin proof tactics.
Suggested BibTeX entry:
@inproceedings{RE99,
author = {C. R{\"o}ckl and J. Esparza},
booktitle = {Proc. of CONCUR'99},
editor = {J. C. M. Baeten and S. Mauw},
number = {1664},
pages = {525540},
publisher = {{SpringerVerlag}},
series = {{Lecture Notes in Computer Science}},
title = {ProofChecking Protocols Using Bisimulations},
year = {1999}
}




