Network Semantics
HTML TeX Standard ML OCaml PostScript C Other
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Failed to load latest commit information.
HOLDoc ignore Mar 19, 2016
specification allow for sock.is2 = NONE and sock.ps2 = NONE in a trace record Jun 30, 2017
test update mktraceindex Aug 8, 2017

Network Semantics

This repository contains the formal specification of TCP, UDP, and the Sockets API developed in the Netsem project:

It has been relicensed under the simplified BSD license. Currently (2015), it is revived using contemporary systems (newer HOL4, PolyML, DTrace, ..)

The demo-traces/ directory contains some example traces (state is unclear)

The HOLDoc/ directory contains tools to typeset the specification (compiles and works).

The notes/ directory contains (meeting and other random) notes.

The specification/ directory contains the segment-level HOL4 specification (previously called Spec1).

The test/ directory contains the test generation and checking tools.

The unmaintained/ directory contains unmaintained specifications, the Lem port of the specifications, etc.


  • Get PolyML (5.5.2 works fine)
  • Get HOL (69fd18990913826ed08e76f768e703515de9c806 from 5th April 2017 works fine)
  • Building specification: cd specification ; $HOL/bin/Holmake
  • Building documentation: cd HOLDoc/src ; $HOL/bin/Holmake followed by cd specification ; $HOL/bin/Holmake TCP1_net1Theory.ui TCP1_netTheory.ui ; make alldoc
  • Building test tools (required OCaml (tested with 4.02.3)): cd test ; make depend OCAMLPATH=~/.opam/4.02.3/bin ; make OCAMLPATH=~/.opam/4.02.3/bin