Program Verification for Optimized Byte Copy
Edoardo Biagioni

We present a program to copy bytes, together with a formal
specification and a proof that the code satisfies the specification.
The program, which is in the critical path for a network
implementation, has been tuned  carefully over a period of time;  the
proof covers the entire program, and is easily updated if the program
is modified.  The program is written in the Standard ML programming
language and was produced as part of the Fox Project implementation of
the TCP/IP protocol suite.