Sat 22 Jun 2019 14:00 - 14:30 at 106B - Modular Reasoning Chair(s): Benjamin C. Pierce

Modular programs require modular specifications, but mechanisms for modularly structuring C programs are less advanced than for more modern languages. This talk will investigate specification patterns inspired by (behavioral) subtyping and abstract data types and show how proofs of separetely specified compilation units in VST can be combined to obtain whole program soundness guarantees.

Sat 22 Jun

Displayed time zone: Tijuana, Baja California change

14:00 - 15:30
Modular ReasoningDeepSpec at 106B
Chair(s): Benjamin C. Pierce University of Pennsylvania
14:00
30m
Talk
Abstraction, Subsumption, and Linking in VST
DeepSpec
Lennart Beringer Princeton University, Andrew Appel Princeton
14:30
30m
Talk
Compositional Verification of Preemptive OS Kernels with Temporal and Spatial Isolation
DeepSpec
Mengqi Liu Yale University
15:00
30m
Talk
Modular Correctness Proofs at the Hardware-Software Interface
DeepSpec
Joonwon Choi Massachusetts Institute of Technology, USA