From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server
We present the first formal verification of a networked server implemented in C. Interaction trees, a general structure for representing reactive computations, are used to tie together disparate verification and testing tools (Coq, VST, and QuickChick) and to axiomatize the behavior of the operating-system on which the server runs (CertiKOS). The main theorem connects a specification of acceptable server behaviors, written in a straightforward “one client at a time” style, with the CompCert semantics of the C program. The variability introduced by low-level buffering of messages and interleaving of multiple TCP connections is captured using network refinement, a variant of observational refinement.
Mon 14 Jan
|14:00 - 14:30|
Ian RoessleVirginia Tech, USA, Freek VerbeekOpen University of the Netherlands, The Netherlands, Binoy RavindranVirginia TechDOI
|14:30 - 15:00|
|15:00 - 15:30|
Nicolas Koh, Yao LiUniversity of Pennsylvania, Yishuai LiUniversity of Pennsylvania, Li-yao Xia, Lennart BeringerPrinceton University, Wolf Honore, William ManskyUniversity of Illinois at Chicago, Benjamin C. PierceUniversity of Pennsylvania, Steve ZdancewicUniversity of PennsylvaniaDOI Pre-print