Dr Douglas R. Smith and
Dr. Christoph Kreitz
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.