Invited Speakers

Unifying speaker

Martin Abadi (Google Brain, USA)

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)

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)

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)

Tutorial speakers

Armin Biere Johannes Kepler University, Linz, Austria

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.


Who's online

We have 88 guests and no members online

Site Hosted by