From C to interaction trees: Specifying, verifying, and testing a networked server

Nicolas Koh, Yao Li, Yishuai Li, Li Yao Xia, Lennart Beringer, Wolf Honoré, William Mansky, Benjamin C. Pierce, Steve Zdancewic

Research output: Chapter in Book/Report/Conference proceedingConference contribution

38 Scopus citations

Abstract

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.

Original languageEnglish (US)
Title of host publicationCPP 2019 - Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with POPL 2019
EditorsAssia Mahboubi
PublisherAssociation for Computing Machinery, Inc
Pages234-248
Number of pages15
ISBN (Electronic)9781450362221
DOIs
StatePublished - Jan 14 2019
Event8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019 - Cascais, Portugal
Duration: Jan 14 2019Jan 15 2019

Publication series

NameCPP 2019 - Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with POPL 2019

Conference

Conference8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019
Country/TerritoryPortugal
CityCascais
Period1/14/191/15/19

All Science Journal Classification (ASJC) codes

  • Computer Science Applications
  • Software

Keywords

  • formal verification
  • interaction trees
  • network refinement
  • QuickChick
  • TCP
  • testing
  • VST

Fingerprint

Dive into the research topics of 'From C to interaction trees: Specifying, verifying, and testing a networked server'. Together they form a unique fingerprint.

Cite this