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.
|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.