Invited Talks and Tutorials
Monday April 4th, 09h00 - 10h00 / Room: Blauwe Zaal
Unifying invited lecture:
Andrew D. Gordon (MSR Cambridge and University of Edinburgh, UK)
Structure and Interpretation of Probabilistic Programs 
Abstract: Probabilistic programming is a technique for solving statistical inference and machine learning problems by writing short pieces of code to model data. We survey the area and describe recent advances in semantic interpretation. Probabilistic programs exhibit structures that include hierarchies of random variables corresponding to the data schema, recurring modelling patterns, and also the classical Bayesian distinction between prior and likelihood. We exploit this structure in language designs that yield data insights with only a modicum of user input.
Tuesday April 5th, 09h00 - 10h00 / Room: Blauwe Zaal
POST invited lecture:
Vitaly Shmatikov (Cornell Tech, USA)
Machine Learning and Privacy: Friends or Foes?
Abstract: Machine learning is eating the world. Modern machine learning methods, especially deep learning based on artificial neural networks, rely on the training data collected from millions of users to achieve unprecedented accuracy and enable powerful AI-based services.
In this talk, I will discuss the complex relationship between machine learning and digital privacy. This includes new threats, such as adversarial use of machine learning to recover hidden user data, and new benefits, such as privacy-preserving machine learning that protects the confidentiality of training data while constructing accurate models.
Tuesday April 5th, 14h00 - 15h00 / Room: Blauwe Zaal
ESOP invited lecture:
Cristina Lopes (University of California at Irvine, USA)
Simulating Cities: A Software Engineering Perspective
Abstract:Despite all the reasons why complex simulations are desirable for decision and policy making, and despite advances in computing power, large distributed simulations of urban areas are still rarely used, with most of their adoption in military applications. The reality is that developing distributed simulations is much harder than developing non-distributed, specialized ones, and requires a much higher level of software engineering expertise.
This talk looks at urban simulations from a software engineering and systems design perspective, and puts forward the idea that non-traditional decompositions in simulation load management are not just beneficial for these applications, but are likely the only way to move that field forward.
Wednesday April 6th, 09h00 - 10h00 / Room: Blauwe Zaal
FASE invited lecture:
Oscar Nierstrasz (Universität Bern, Switzerland)
The Death of Object-Oriented Programming
Abstract: Modern software systems are increasingly long-lived. In order to gracefully evolve these systems as they address new requirements, developers need to navigate effectively between domain concepts and the code that addresses those domains. One of the original promises of object-orientation was that the same object-oriented models would be used throughout requirements analysis, design and implementation. Software systems today however are commonly constructed from a heterogeneous “language soup” of mainstream code and dedicated DSLs addressing a variety of application and technical domains. Has object-oriented programming outlived its purpose?
We argue that we need to rethink the original goals of object-orientation and their relevance for modern software development. We propose as a driving maxim, “Programming is Modeling,” and explore what this implies for programming languages, tools and environments. In particular, we argue that: (1) source code should serve not only to specify an implementation of a software system, but should encode a queryable and manipulable model of the application and technical domains concerned; (2) IDEs should exploit these domain models to enable inexpensive browsing, querying and analysis by developers; and (3) barriers between the code base, the running application, and the software ecosystem at large need to be broken down, and their connections exploited and monitored to support developers in comprehension and evolution tasks.
Thursday April 7th, 09h00 - 10h00 / Room: Blauwe Zaal
Unifying invited lecture:
Rupak Majumdar (MPI Kaiserslautern, Germany)
Robots at the Edge of the Cloud
Abstract: Computers have come a long way from their roots as fast calculating devices. We live in a world in which computers collect, store, and analyze huge volumes of data. We are seeing the beginnings of a new revolution in the use of computers. In addition to collecting and analyzing data, computers are influencing the physical world and interacting autonomously, and in complex ways, with large groups of humans. These cyber-physical-social systems have the potential to dramatically alter the way we lead our lives. However, designing these systems in a reliable way is a difficult problem. In this talk, we enumerate a set of research challenges that have to be overcome in order to realize the potential of cyber-physical-social systems.
Invited tutorials:
Monday April 4th, 16h30 - 18h00 / Room: CZ 8
Peter Ryan (University of Luxembourg, Luxembourg)
The Design and Analysis of End-to End Verifiable Voting Systems
Abstract: Elections form the foundation of democracy, and from the dawn of democracy they have been the target of attack by parties wanting to manipulate the outcome. From a security perspective they constitute a fascinating and fertile terrain to explore. Over time voting systems have evolved various mechanisms to ensure the accuracy of the outcome and guarantee the privacy of votes. However, with the advent of digital technologies a whole raft of new threats have emerged, in many cases introducing possibilities of wholesale fraud. This became particularly acute with the deployment of touch-screen voting devices in the US. Here the the accurate recording and transmission of votes is whole dependent of the correctness of the software running on the devices. Internet voting faces even more severe threats.
Such concerns motivated the crypto and security communities to take up the challenge of making voting secure in the digital era. Particularly over the last decade or so significant strides have been made in the design, analysis and to some extent deployment of so called “end-to-end verifiable” schemes: that provide voters with the means to verify that their vote is accurately counted while avoiding vote-buying or coercion threats. Voting systems are complex polio-technical systems with rich and subtle properties. Virtually all the tricks and tools in the cryptographer’s toolkit have found application here. In this tutorial I will describe the security challenges and present some of the more prominent schemes that have been developed recently, both for in-person and internet voting. I will present some of the key cryptographic mechanisms and the security goals, threat models. In particular i will trace the evolution of the Pret a Voter system from the original concept in 2004 to the vVote system that was deployed for Lower House elections in the State of Victoria in Australia in November 2014. I will conclude with open questions and challenges.
Wednesday April 6th, 16h30 - 18h00 / Room: CZ 7
Grigore Rosu (University of Illinois at Urbana-Champaign, USA)
K: a semantic framework for programming languages and formal analysis tools
Abstract: K (http://kframework.org) is a rewrite-based executable semantic framework in which programming languages, type systems and formal analysis tools can be defined using configurations, computations and rules. Configurations organize the state in units called cells, which are labeled and can be nested. Computations carry computational meaning as special nested list structures sequentializing computational tasks, such as fragments of program. Computations extend the original language abstract syntax. K (rewrite) rules make it explicit which parts of the term they read-only, write-only, read-write, or do not care about. This makes K suitable for defining truly concurrent languages even in the presence of sharing. Computations are like any other terms in a rewriting environment: they can be matched, moved from one place to another, modified, or deleted. This makes K suitable for defining control-intensive features such as abrupt termination, exceptions or call/cc. Several real languages have been defined in K, such as C (ISO C11 standard), Java (1.4), JavaScript (ES5), Python, Scheme, Verilog, and dozens of prototypical or classroom ones. The ISO C11 semantics and a fast OCAML backend for K power RV-Match (https://runtimeverification.com/match), one of the most advanced commercial automated analysis tools for C.
The tutorial attendees will learn how to define a language or a type system in K, and then how to use that definition to get an executable model of the defined language or system which is amenable for formal analysis.