Invited Talks and Tutorials
Unifying speaker
Martin Abadi (Google Brain, USA)
Speech not available
Title: On the Theory and Practice of Software that Learns
As machine learning becomes more powerful and pervasive, it has an impact on the many software systems that rely on it and on the underlying software and hardware platforms. The resulting questions should concern virtually all aspects of ETAPS, as they relate to software engineering, security and trust, programming, tools, foundations, and more. This talk will discuss some of those questions. In particular, it will present recent research on the semantics of programming languages suitable for learning by gradient descent and on adversarial machine learning.
FASE invited speaker
Pamela Zave (AT&T Labs, USA)
View speech
Title: When the model really matters: The compositional architecture of the Internet
In 1992 the explosive growth of the World Wide Web began. In 1993 the last major change was made to the ``classic'' Internet architecture. Since then the Internet has been adapted to handle a truly impressive list of additional applications and unforeseen challenges, at global scale. Although the architecture of the Internet has changed completely, the way that experts think and talk about it has not changed. The result is runaway complexity in networking, and an academic field based on accumulation of detail rather than principles.
This talk introduces a new formal model for networking, based on flexible composition of modular networks. Each module is a microcosm of networking, with all the basic structures and mechanisms. The new model provides faithful descriptions of how the Internet works today, as well as principles that support (1) re-use of solution patterns at different scopes and levels of abstraction, (2) interoperation with new designs and evolution toward them, and (3) verification of trustworthy network services.
Technological advances are rapidly making most network hardware programmable. This has attracted the interest of researchers from the programming-languages and verification communities. The new model greatly expands the set of network phenomena that can be studied rigorously, formalized, and verified. In doing so, the new model will provide broader opportunities for formal methods to contribute to the trustworthiness of globally distributed computer systems.
POST invited speaker
Benjamin C. Pierce (University of Pennsylvania, USA)
View speech
Title: The Science of Deep Specification
Abstraction and modularity underlie all successful hardware and software systems: We build complex artifacts by decomposing them into parts that can be understood separately. Modular decomposition depends crucially on the artful choice of interfaces between pieces. As these interfaces become more expressive, we think of them as specifications of components or layers. Rich specifications based on formal logic are little used in industry today, but a practical platform for working with them could signicantly reduce the costs of system implementation and evolution by identifying vulnerabilities, helping programmers understand the behavior of new components, facilitating rigorous change-impact analysis, and supporting maintainable machine-checked verication that components are correct and fit together correctly.
Recently, research in the area has begun to focus on a particularly rich class of specifications, which might be called deep specifications. Deep specifications are rich (describing complex component behaviors in detail); two-sided (connected to both implementations and clients); formal (written in a mathematical notation with clear semantics to support tools such as type checkers, analysis and testing tools, automated or machine-assisted provers, and advanced IDEs); and live (connected directly to the source code of implementations via machine-checkable proofs or property-based random testing). These requirements impose strong functional correctness conditions on individual components and permit them to be connected together with rigorous composition theorems.
This talk presents the key features of deep specifications, surveys recent achievements and ongoing efforts in the research community (in particular, work at Penn, Princeton, Yale, and MIT on formalizing a rich interconnected collection of deep specifications for critical system software components), and argues that the time is ripe for an intensive effort in this area, involving both academia and industry and integrating research, education, and community building. The ultimate goal is to provide rigorously checked proofs about much larger artifacts than are feasible today, based on decomposition of proof effort across components with deep specifications.
ESOP invited speaker
Derek Dreyer (MPI-SWS, Germany)
View speech
Title: RustBelt: Logical Foundations for the Future of Safe Systems Programming
Rust is a new systems programming language, developed at Mozilla, that promises to overcome the seemingly fundamental tradeoff in language design between high-level safety guarantees and low-level control over resource management. Unfortunately, none of Rust's safety claims have been formally proven, and there is good reason to question whether they actually hold. Specifically, Rust employs a strong, ownership-based type system, but then extends the expressive power of this core type system through libraries that internally use unsafe features.
In this talk, I will present RustBelt (http://plv.mpi-sws.org/rustbelt), the first formal (and machine-checked) safety proof for a language representing a realistic subset of Rust. Our proof is extensible in the sense that, for each new Rust library that uses unsafe features, we can say what verification condition it must satisfy in order for it to be deemed a safe extension to the language. We have carried out this verification for some of the most important libraries that are used throughout the Rust ecosystem.
After reviewing some essential features of the Rust language, I will describe the high-level structure of the RustBelt verification and then delve into detail about the secret weapon that makes RustBelt possible: the Iris framework for higher-order concurrent separation logic in Coq (http://iris-project.org). I will explain by example how Iris generalizes the expressive power of O'Hearn's original concurrent separation logic in ways that are essential for verifying the safety of Rust libraries. I will not assume any prior familiarity with concurrent separation logic or Rust.
This is joint work with Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and the rest of the Iris team.
Tutorial speakers
Armin Biere Johannes Kepler University, Linz, Austria
View speech
Title: Searching, Simplifying, Proving. A Tutorial on Modern SAT Solving.
This tutorial covers algorithmic aspects of conflict-driven clause learning and important extensions developed in recent years, including decision heuristics, restart schemes, various pre- and inprocessing techniques as well as proof generation and checking. Programmatic incremental usage of SAT solvers is discussed next. The talk closes with an overview on the state-of-the-art in parallel SAT solving and open challenges in general.
The speaker contributed to the core technology of modern SAT solving, has developed 12 SAT solvers since 1999, which won 36 medals including 16 gold medals in international SAT competitions.
Fabio Somenzi University of Colorado, Boulder, U.S.A.
View speech
