Proof-checking an audio control protocol with LP

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.

Additional Metadata
ACM	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)
MSC	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)
Publisher	CWI
Series	Department of Computer Science [CS]
Citation APA Style AAA Style APA Style Cell Style Chicago Style Harvard Style IEEE Style MLA Style Nature Style Vancouver Style American-Institute-of-Physics Style Council-of-Science-Editors Style BibTex Format Endnote Format RIS Format CSL Format DOIs only Format	Griffioen, W. O. D. (1995). Proof-checking an audio control protocol with LP. Department of Computer Science [CS]. CWI.

Publication