HACMS Project

Principal Investigators: Dr. Douglas R. Smith and Dr. Christoph Kreitz

Objective:

Kestrel Institute is developing high-assurance implementations of a TCP/IP network protocol stack. The high-level protocol is specified in Specware, and then the Specware refinement transformation tool chain is used to synthesize an efficient implementation. Formal correctness proofs, in the Isabelle Isar proof assistant, are generated during the transformation process.