Amal Ahmed (Northeastern University, USA)

Picture of Amal Ahmed

Title: Compositional Compiler Verification for a Multi-Language World

Abstract: Verified compilers are typically proved correct under severe restrictions on what the compiled code may be linked with, from no linking at all to linking with only the output of the same compiler. Unfortunately, such assumptions don’t match the reality of how we use these compilers as most software today is comprised of components written in different languages compiled by different compilers to a common target. A key challenge when verifying correct compilation of components — or “compositional” compiler correctness — is how to formally state the compiler correctness theorem so it supports linking with target code of arbitrary provenance, as well as verification of multi-pass compilers. Recent results state their correct-component-compilation theorems in remarkably different ways. Worse, to check if these theorems are sensible, reviewers must understand a massive amount of formalism.

In this talk, I will survey recent results, explaining pros and cons of their compiler-correctness statements, and then present a generic compositional compiler correctness (CCC) theorem that we argue is the desired theorem for any compositionally correct compiler. Specific compiler-verification efforts can use their choice of formalism “under the hood” and then show that their theorems imply CCC. I’ll discuss what CCC reveals about desired properties of proof architectures going forward. In particular, I’ll explain why compositional compiler correctness is, in essence, a language interoperability problem and that building truly compositional verified compilers demands that we design languages that give programmers control over a range of interoperability (linking) options.

Speaker Bio: Amal Ahmed is an Associate Professor of Computer Science at Northeastern University.  Her research interests include type systems and semantics, compiler verification, language interoperability, dependent types, and gradual typing.  She is known for her work on scaling the logical relations proof method to realistic languages — with features like memory allocation and mutation, objects, and concurrency — leading to wide use of the technique, e.g., for correctness of compiler transformations, soundness of advanced type systems, and verification of fine-grained concurrent data structures.  Her primary focus of late has been on developing an architecture for building correct and secure compilers that support safe inter-language linking of compiled code.  Her awards include an NSF Career Award and a Google Faculty Research Award.  She has served as program chair for ESOP and on the steering committees of ETAPS, ESOP, PLMW, and ICFP.  She is also a frequent lecturer at the annual Oregon Programming Languages Summer School (OPLSS).

Isil Dillig (University of Texas, Austin, USA)

Picture of Isil Dillig

Title: Program Synthesis using Conflict-Driven Learning

Abstract: In recent years, there has been a flurry of interest in program synthesis, where the goal is to automatically generate a program that satisfies some high-level specification. While program synthesis has proven to be very useful for automating a diverse class of tasks, most synthesis algorithms target a specific application and cannot be reused across different domains. In this talk, we will introduce a meta-synthesis algorithm that can be instantiated for many different domains using a small amount of domain knowledge provided by an expert. The key idea is to combine statistical and logical reasoning in a synergistic way, where a stastical model is used to guide search and logical reasoning is used to dramatically prune the search space by automatically learning userful information from failed synthesis attempts (i.e., conflicts).

Speaker Bio: Isil Dillig is an Associate Professor of Computer Science at the University of Texas at Austin where she leads the UToPiA research group. Her current research interests include program analysis, synthesis, and automated logical reasoning. Dr. Dillig is a Sloan Fellow and a recipient of an NSF CAREER award. Her research has been recognized with various awards, such as PLDI and OOPSLA distinguished paper awards, an ETAPS best award, and a CACM research highlight distinction. Outside of work, she enjoys hiking, scuba diving, and photography.

Viktor Vafeiadis (MPI-SWS, Germany)

Picture of Viktor Vafeiadis

Title: Correctness in a weakly consistent setting

Abstract: In the multicore/multiprocessor setting, different threads have diverging views of the shared memory, which are only weakly consistent with one another. For example, threads A and B may disagree on the order that two shared memory operations have happened; say A has seen the effect of operation C but not of operation D, while B has seen the effect of D but not of C. There has been a lot of work of specifying exactly how different can the views of two threads be–both at the architecture level with formal models for x86, ARM, and Power, and the programming language level with the C/C++ and Java memory models. In this talk, I will discuss what all this work entails for program correctness. How can we specify a concurrent library, say a queue or a set, in the weak memory model setting? What reasoning principles can we use to verify such a library?

Speaker Bio: Viktor Vafeiadis is a tenured faculty member at the Max Planck Institute for Software Systems (MPI-SWS). He got his PhD from the University of Cambridge in 2008, working on the combination of separation logic and rely-guarantee reasoning, for which he received the ACM SIGPLAN distinguished dissertation award. After postdoc positions at Microsoft Research and at the University of Cambridge, in October 2010 he joined MPI-SWS, where he has worked on verified compilation and weak memory concurrency.