Principles of Programming Seminar
— 4:00pm
Location:
In Person
-
Traffic21 Classroom Gates Hillman 6501
Speaker:
MICHAEL SAMMLER
,
Ph.D. Student, Max Planck Institute for Software System, and Saarland Informatics Campus
https://people.mpi-sws.org/~msammler/
DimSum: A Decentralized Approach to Multi-language Semantics and Verification
Programs are often not written in a single language but consist of components written in multiple different languages. However, verifying such multi-language programs proves to be a daunting task as the existing approaches to this problem impose a variety of restrictions on the overall structure of multi-language programs (e.g. fixing the source language, fixing the set of involved languages, fixing the memory model, or fixing the semantics of interoperation). In this talk, I show how one can combine ideas from different areas including process calculi, wrappers, and dual non-determinism to build a novel, decentralized approach for multi-language semantics and verification.
This approach, called DimSum, allows defining and reasoning about languages independently from each other (as independent modules communicating via events), but also combining and translating between them when necessary (via a library of combinators). The talk presents DimSum based on a high-level imperative language Rec (with an abstract memory model and function calls), a low-level assembly language Asm (with a concrete memory model, arbitrary jumps, and syscalls), and a mathematical specification language Spec.
Concretely, the talk is based around the example of a Rec program that is linked with an Asm library providing the ability to compare pointers and the talk uses this example to illustrate the core components of DimSum, including semantic linking using events, wrappers, and dual non-determinism.
— Michael Sammler is a PhD student at the Max Planck Institute for Software Systems under the supervision of Deepak Garg and Derek Dreyer. His research focuses on developing techniques for formal verification of realistic low-level systems software that combine machine-checked proofs with a high degree of automation. He has received multiple awards for his research, including Distinguished Paper awards at PLDI and POPL and a Google PhD fellowship.
Faculty Host: Jan Hoffmann
Event Website:
https://www.cs.cmu.edu/Groups/pop/index.html