Most methods of data transmission and storage are prone to errors, leading to data loss. Error-correcting codes encode the data with redundant parity information to allow the original data to be recovered even in the presence of a small number of errors. An erasure code uses an ECC to correct erasures, errors where the location is known. There are dozens of classes of error-correcting and erasure codes, many based on sophisticated mathematics, making them difficult to verify using automated tools.

These erasure codes can be implemented in networks as Forward Erasure Correction, in which a sender encodes a block of input packets using an ECC, and the receiver decodes if errors were detected. In this talk, I will describe my verification of a real-world C implementation of FEC using Coq and the Verified Software Toolchain for verifying C programs. This verification includes both a purely-mathematical proof that the underlying algorithm (a form of Reed-Solomon erasure coding) is correct and the VST proof that the C code, over 25 years old and including many modifications and optimizations, correctly implements this algorithm.

Reading list:

Everyone is invited to attend the talk, and those faculty wishing to remain for the oral exam following are welcome to do so.