ETAPS 2021: 27 March-1 April 2021, Luxembourg, Luxembourg (online)

Invited Talks and Tutorials

The invited speakers and tutorialists from ETAPS 2020 (cancelled because of the pandemic) have been reinvited to speak at ETAPS 2021.

Unifying speakers

Scott Smolka, Stony Brook University, USA

Title: A Bird's-Eye View of Flocking

Abstract: In this talk, I will discuss recent advances in computational approaches to flocking behavior in multi-agent systems. The talk will be in three parts. In the first part, I will present Declarative Flocking (DF), our approach to the flocking problem based on optimal control, Model Predictive Control in particular. DF allows us to capture various aspects of flocking behavior (basic flocking, target seeking, predator avoidance, etc.) simply as terms of a cost function. In the second part, I will present our work on Neural Flocking (NF) which demonstrates how a symmetric and fully distributed flocking controller can be synthesized using Deep Learning from a centralized flocking controller. Finally, I will discuss how we extend Declarative Flocking to capture high-speed, flock-wide turning maneuvers, a phenomenon seen in starling flocks.

Jane Hillston, University of Edinburgh, United Kingdom

Title: Learning to Improve Quantitative Formal Methods

Abstract: Quantitative formal models incorporate information about timing and probability, allowing the dynamic behaviour of systems to be analysed.  Whilst they can provide useful predictions, the analysis of such models is often computationally expensive.  In the talk I will present a number of ways in which machine learning can be used to improve the efficiency of model analysis.  These techniques work by applying machine learning to the data generated by the model itself.  For example, learning can facilitate model abstraction by identifying a more compact, alternative representation of the dynamics, or can support targeted sampling during statistical model checking to maximise the information gained.


ESOP invited speaker

Isil Dillig, University of Texas at Austin, USA

Title: Computer-Aided Programming Across the Software Stack 

Abstract: Program synthesis techniques aim to generate executable programs from  expressions of user intent. This talk will showcase various applications of program synthesis across different layers of the software stack, starting from computer end-users to application programmers and all the way down to systems programmers. It will also highlight the usefulness of program synthesis for addressing different software concerns, including functionality, correctness, performance, and security.


FASE invited speaker

Willem Visser, Amazon Web Services and Stellenbosch University, South Africa

Title: The Magic of Analysing Programs
Abstract: The presentation will take a brief tour describing various technologies that have proven useful to discover software defects (semi-)automatically. These include model checking, symbolic execution and static dataflow analysis. The final part of the talk will focus on lessons learned from applying static analysis tools to real code at Amazon Web Services.

Tutorial speakers

Erika Ábrahám (RWTH Aachen University, Germany) - on analysis of hybrid systems

Title: Reachability Analysis Techniques for Hybrid Systems

Abstract: In this tutorial we address systems, whose behavior combines discrete and continuous components. Examples for such hybrid systems are automotive systems or digitally controlled physical or chemical plants.

The reachability problem for hybrid systems poses the question whether a state from a given unsafe set can be reached in a hybrid system model from a fixed set of initial states. Though this problem is in general undecidable, there are different techniques that either restrict model expressivity or compute approximations. In this tutorial we discuss available approaches with the focus on flowpipe-construction-based methods, and report on some observations regarding their usage and applicability.

Madhusudan Parthasararathy (University of Illinois at Urbana-Champaign, USA)

Title: Learning Logical Expressions with Applications to Verification, Specification Mining, and Proofs

Abstract: Over the years, the technique of learning logical expressions from data has emerged and found applications to several fields in formal methods and program verification. This tutorial will survey several important learning settings (passive, online, ICE, etc.) for learning logical expressions in logics ranging from propositional logic, quantifier-free logics over theories, and quantified first-order logics, as well as tool frameworks that facilitate such learning. We will also showcase a growing number of applications including synthesizing invariants and contracts for verification, mining software specifications from dynamic executions on test inputs, and learning inductive hypotheses for proving theorems using induction. We will conclude with new interesting open directions for learning logics with applications to interpretable AI.