From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server

Nicolas Koh, Yao Li, Yishuai Li +6

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 toge…