PoP Seminar Talk

DimSum: A Decentralized Approach to Multi-language Semantics and Verification

Michael Sammler, PhD Student at the Max Planck Institute for Software Systems and Saarland Informatics Campus
Friday, 04 November, 2022; 3:00pm
GHC 6501
Host: Jan Hoffmann

Abstract

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.

Bio

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.