In this paper we report on the use of the Larch Prover to mechanize the correctness proof of a version of the Philips Audio Control Protocol.

Network Protocols (acm C.2.2), Local and Wide-Area Networks (acm C.2.5), SPECIAL-PURPOSE AND APPLICATION-BASED SYSTEMS (acm C.3), Software/Program Verification (acm D.2.4), Models of Computation (acm F.1.1)
Classical propositional logic (msc 03B05), Higher-order logic and type theory (msc 03B15), Grammars and rewriting systems (msc 68Q42), Theory of computing (msc 68Qxx), Specification and verification (program logics, model checking, etc.) (msc 68Q60)
Department of Computer Science [CS]

Griffioen, W.O.D. (1995). Proof-checking an audio control protocol with LP. Department of Computer Science [CS]. CWI.