Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Mon 14 Jan 2019 15:00 - 15:30 at Sala XII - Research Papers: Program Verification Chair(s): Chris Hawblitzel

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 - 15:30: CPP 2019 - Research Papers: Program Verification at Sala XII
Chair(s): Chris HawblitzelMicrosoft Research
CPP-201914:00 - 14:30
Research paper
Ian RoessleVirginia Tech, USA, Freek VerbeekOpen University of the Netherlands, The Netherlands, Binoy RavindranVirginia Tech
CPP-201914:30 - 15:00
Research paper
Sandrine BlazyUniv Rennes- IRISA, Rémi HutinIRISA / ENS Rennes
CPP-201915:00 - 15:30
Research paper
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 Pennsylvania
DOI Pre-print