Abstraction, Subsumption, and Linking in VST
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 Times are displayed in time zone: (GMT-07:00) Tijuana, Baja California change
|14:00 - 14:30|
|14:30 - 15:00|
Mengqi LiuYale University
|15:00 - 15:30|
Joonwon ChoiMassachusetts Institute of Technology, USA