Sat 22 Jun 2019 16:20 - 16:45 at 106B - Interaction Trees and Algebraic Effects I Chair(s): Andrew Appel

The Verified Software Toolchain (VST) gives us a powerful tool for proving correctness of C programs. With the recent addition of mechanisms for external state, we can even reason about the behavior of programs that communicate with the outside world, for instance via network sockets or console I/O. But the implementations of these communication functions cannot be verified with VST: they involve the state of the operating system and interactions with device drivers, and break the usual single-program, single-memory abstraction of user-level programs. In this talk, we will present work on connecting VST proofs to system call implementations in CertiKOS, the verified operating system, which uses a different approach to verifying (kernel-level) C code. Such a connection must bridge the gap between VST’s step-indexed, ownership-annotated model of memory and CertiKOS’s more concrete representation, as well as establishing a common language for talking about communication events across user programs and the OS.

Sat 22 Jun

deepspec-2019-papers
16:00 - 17:30: DeepSpec 2019 - Interaction Trees and Algebraic Effects I at 106B
Chair(s): Andrew AppelPrinceton
deepspec-2019-papers16:00 - 16:20
Talk
Steve ZdancewicUniversity of Pennsylvania
deepspec-2019-papers16:20 - 16:45
Talk
William ManskyUniversity of Illinois at Chicago, Wolf Honore
deepspec-2019-papers16:45 - 17:30
Talk
Daan LeijenMicrosoft Research, USA