Proof-checking a data link protocol door L. Helmink