Specifying and Verifying IP with Linear Logic
David Sinclair*, James Power**, and Paul Gibson**, David Gray*, and
Geoff Hamilton*
* Dublin City University, IRELAND
** National University of Ireland, IRELAND
Abstract
This paper presents a specification and verification of the Internet
Protocol (IP) in linear logic.
IP has the essential propoerties of a typical distributed system. This
paper shows how linear
logic can be used to prove some properties of this layer. Both the
specification and the
correctness proofs have been verified using the Coq proof assistant, via
the authors' embedding
of linear logic into this constructive framework.
Keywords:
linear logic, verification, protocols, Coq, theorem proving