List of invited speakers at QONFEST conferences and workshops

Clicking on the name of a speaker provides more details about their talk.

Patricia Bouyer-Decitre – CNRS, LMF, France

Invited Speaker for the Concur conference
Thursday August 26, 2021, 12:00–13:00 CEST

Parameterized concurrent games

Abstract: Game theory has shown its usefulness for expressing and then solving many problems in verification. Indeed strategies in games can be interpreted as controllers or programs, which dictate which actions should be done by a system. Various solution concepts allow to capture various kinds of desirable behaviours of such a system (winning strategies, Nash equilibria, etc.). Standard concurrent graph games assume a fixed number of players, which interact and altogether generate a play. When the number of players is a priori unknown, such concurrent games with a fixed number of players are no more appropriate. We therefore propose the model of parameterized concurrent games played on a graph, where the number of players can be arbitrary. Several questions of interest can be asked on this model, like the existence of winning strategies for a designated player, whatever the number of opponents; or the existence of a joint cooperative strategy profile for the players, in order to achieve some goal. In this talk I will report on general results on concurrent games, I will present the model of parameterized concurrent games and show preliminary results on this model. This is based on joint works with Nathalie Bertrand and Anirban Majumdar.

Short Bio: Patricia Bouyer-Decitre holds a PhD in Computer Science from ENS Cachan (2002). She has been a CNRS researcher from 2002 to 2020 at "Laboratoire Spécification et Vérification" (LSV, CNRS & ENS Cachan, France). She is now the head of the newly created "Laboratoire Méthodes Formelles" (LMF, Université Paris-Saclay, CNRS, ENS Paris-Saclay, France). She has held visiting positions at Aalborg University (Denmark) in 2002 and Oxford University (UK) in 2007. Patricia Bouyer-Decitre's main research topics are model checking, game theory, and quantitative aspects of verification. She has been the principal investigator of ERC Starting Grant project EQualIS (2013-2019). She was the recipient of a Marie Curie fellowship in 2006, of the Bronze medal of CNRS in 2007 and of the Presburger Award given by the EATCS in 2011.

François Baccelli – University of Texas at Austin

Invited Speaker for the Qest conference
Wednesday August 25, 2021, 15:45–16:45 CEST

Stochastic Geometry based Performance Analysis of Wireless Networks

Abstract: Stochastic Geometry is commonly used for analyzing spectrum sharing in large wireless networks. In this approach, network elements, such as users and base stations, are represented as point processes in the Euclidean plane, and interference fields as spatial shot-noise processes. The analytical machinery of stochastic geometry and basic formulas of information theory can then be combined to predict important spatial statistics of such networks. The talk will first exemplify this approach by showing how to derive the distribution of the Shannon rates obtained by users in two fundamental models, the Poisson dipole model, which is a mathematical abstraction for a large device to device network, and the Poisson-Voronoi model which is an abstraction for a large cellular network. A few variants of these now classical models will be also discussed, like multi-tier cellular networks, or networks leveraging beam-forming. The talk will then exemplify how to introduce birth-and-death type dynamics in this stochastic geometry framework. This will be illustrated through recent results on the simplest model in this class. In this model, users arrive according to a Poisson rain process on the Euclidean plane and leave with a stochastic intensity proportional to their instantaneous Shannon rate.

Joe Kiniry – Galois Inc. and Free & Fair

Invited Speaker for the FMICS conference
Tuesday August 24, 2021, 18:30–19:30 CEST

Haunting Tales of Applied Formal Methods from Academia and Industry

Abstract: You learn a lot after being a formal methods researcher and practitioner for 25 years. Half of that time was spent in academia, creating formal processes, methodologies, and tools that I hoped I could secretly impact engineers. Half of that time has been spent in industry, working at companies to transition concept, tools, and technologies in rigorous digital engineering (RDE) with applied formal methods. These days I work at two companies, Galois and Free & Fair, leading R&D in RDE that focus on problems in national security and nationally critical infrastructure. I also work with many of our other Galois spin-outs, such as Muse (now Sonotype Lift) and Niobium Microsystems on these same topics. In this talk I’ll tell a small number of stories about these many years in the field, each of which has, I hope, an actionable nugget of wisdom for the audience at FMICS.

Short Bio: Dr. Joe Kiniry is a Principal Scientist at Galois and is the CEO and Chief Scientist at Free & Fair.  Over the past twenty five years he has been everything from a tenured professor at several universities to a founder and chief scientist or CTO at several companies.  He has been involved in security in some fashion since the early 80s when he hacked and wrote video games on 8 bit computers.  These days, his day job is applying formal methods to hardware security for the DoD and trying to help the worlds’ elections and democracies be more trustworthy.

Boudewijn Haverkort – Tilburg University

Joint Invited Speaker for Concur and Qest conferences
Tuesday August 24, 2021, 15:45–16:45 CEST

Performance Evaluation: Model or Problem Driven?

Abstract: Going back as far as the mid 1960s, a variety of performance evaluation techniques have been proposed and used to help solve design and dimensioning questions for computer systems and networks. In the 1970s a number of workshops on the topic of computer performance evaluation started to emerge, that over the years evolved into successful conference series that last until today. Performance Evaluation has been a well-acclaimed journal since the beginning of the 1980s. However, some researchers also claim that the field of performance evaluation has developed too much independently from the development of the systems it intends to evaluate, leading to a fairly isolated sub-discipline that not always addresses the questions that really are important. In the first part of my talk I address this claim, which I consider to be true to a large extend, try to analyse why the field has evolved in this way, and do a number of suggestions for overcoming this isolation. In the second part of my talk, I will touch upon a number a recent modelling efforts I have been involved in myself, in which we have tried to be problem-driven, rather than model-driven.

Short Bio: Boudewijn Haverkort is an experienced academic in the field of the design and application of all sorts of computer systems, having worked in leadership roles in the Netherlands (at the University of Twente the Embedded Systems Institute, and, currently, Tilburg University) and Germany (at the RWTH Aachen), and in a large number of international (European as well as nationally funded) research and innovation projects. Fields of application he has worked in include wireless and wearable communication systems, internet-based systems, smart industry, smart grids, energy efficient data centers and cyber-security of industrial systems. The applications he prefers to work at relate to the great societal challenges we are facing: sustainability, mobility, and safety & security. He has published some 200 scientific papers in journals and at conferences, and held leadership roles in many international conferences. Numerous MSc students as well as 30+ PhD students graduated under his supervision. He is well-versed in governance and leadership roles in higher education institutions, as well as in public-private partnerships. Boudewijn has been director of the independent open innovation institute on Embedded Systems Engineering (2009-2013; now part of TNO), head of the department of computer science at the University of Twente (2008-2009 and 2017-2018) and serves as chairman of the national research and innovation program on big data and its applications (Commit2Data) since 2016. January 2019, he started as dean for the Tilburg School of Humanities and Digital Sciences. In his (rare) spare time, he finds inspiration in art, music, architecture, literature, mountain walking, and mountain biking.

Daniele Magazzeni – King's College, London & JP Morgan AI Research

Invited Speaker for the FORMATS conference
Tuesday August 24, 2021, 12:00–13:00 CEST

Temporal Reasoning for Intelligent Financial Services: Examples and Challenges

Abstract: Temporal reasoning can play a key role in the financial domain. In this talk, I will present several research directions we are pursuing and discuss how temporal reasoning can help in a variety of problems faced by large financial institutions. Active research activities include efficient resource allocations, time series analysis, behavioural reasoning, fraud detection, and market predictions. I will offer concrete examples of projects, presenting the contributions and highlighting the main challenges. I will then focus on a more specific area that has strong implications for temporal reasoning, namely Explainable AI (XAI). XAI represents an increasingly critical feature of operations undertaken within the financial industry, as brought about by the growing sophistication of AI models and the demand for fairness, safety and interpretability. I will present some novel XAI techniques we developed that leverage temporal reasoning, and future directions. I will conclude highlighting the many challenges and opportunities for temporal reasoning in the financial domain.

Short Bio: Dr. Daniele Magazzeni is a Research Director at J.P. Morgan AI Research where he is also the Head of the firmwide Explainable AI Center of Excellence. His main research interests are in AI Planning and Machine Learning for efficient resource allocation and processes optimization, and Explainable AI. Daniele is the current President of the International Conference on Automated Planning and Scheduling (ICAPS). Daniele is Associate Professor (on leave) at King’s College London, where he was Co-Director of the UK Center for Doctoral Training in Safe and Trusted AI, and Head of the Human-AI-Teaming Lab. He is a frequent tutorial and keynote speaker at AI Conferences.

Jana Tumova – KTH Royal Institute of Technology, Stockholm

Invited Speaker for the FORMATS conference
Thursday August 26, 2021, 15:45–16:45 CEST

Formal methods for robot motion planning with time and space constraints

Abstract: Autonomous robots have permeated a variety of application areas from industrial automation to transport to household services. Robot vacuum cleaners clean our homes and mobile robotic solutions have been deployed in warehouses to carry shelves of goods. Gradually, autonomous mobile robots are moving from enclosed environment to our everyday lives. How can we ensure that they work as expected and how can we even specify what it means to work as expected? In this talk, we will discuss robot motion planning problem with complex tasks, time and space constraints expressed in temporal logic, such as metric temporal logic or signal temporal logic. We will present solutions that combine sampling-based motion planning with formal methods approaches and yield certain provable guarantees on the satisfaction of the given specifications. Finally, we will show several application examples ranging from autonomous driving with traffic rules to exploration of unknown environments with UAVs.

Short Bio: Jana Tumova is an associate professor at the School of Electrical Engineering and Computer Science at KTH Royal Institute of Technology. She received PhD in computer science from Masaryk University and was awarded ACCESS postdoctoral fellowship at KTH in 2013. She was also a visiting researcher at MIT, Boston University, and Singapore-MIT Alliance for Research and Technology. Her research interests include formal methods applied in decision making, motion planning, and control of autonomous systems. Among other projects, she is a recipient of a Swedish Research Council Starting Grant to explore compositional planning for multi-agent systems under temporal logic goals and a WASP Expeditions project focusing on design of socially acceptable and correct-by-design autonomous systems.

Davide Sangiorgi – University of Bologna

Invited Speaker for the CONCUR conference
Friday August 27, 2021, 15:45–16:45 CEST

From Enhanced Coinduction towards Enhanced Induction

Abstract: The bisimulation proof method and its enhancements have had a profound impact on the success of bisimilarity. There exist a rich and well-developed theory of such enhancements, which has also been lifted to the more abstract setting of coinduction. Sometimes the enhancements seem essential to be able to carry out a proof: defining a full bisimulation, with all needed pairs, can be considerably hard, let alone carrying out the whole proof. This is particularly frequent in languages with higher-order constructs or constructs for mobility (e.g., languages encompassing features from the lambda-calculus and the pi-calculus).
As a behavioural equivalence, however, bisimilarity has also been criticised. One of the main arguments is that it may be regarded as too fine, discriminating processes that an observer could not tell apart. Another argument against bisimilarity is that it does not have a natural associated preorder. Various behavioural relations, both preorders and equivalences, have been studied that improve on such limitations, e.g., trace, failure, ready-set, refusal, and testing relations. We may call such relations `inductive' because generally rooted on observables that are inductively-defined, such as enriched forms of traces.
In the talk I will review the theories of bisimulation enhancements and I will discuss an attempt at transferring the bisimulation enhancements onto the realm of inductive behavioural relations.

Jan Friso Groote – Eindhoven University of Technology

Invited Speaker for the Express/SOS workshop
Monday August 23, 2021, 9:00–10:00 CEST

The real hotel. A problem with infinite choice and continuous distributions

Abstract: Process algebras with data generally have an infinite choice construct that can for instance be used to model selecting or reading data, such as reading a real number. It is tempting to enhance such process algebras with probabilities, or even better, continuous probability distributions. As it stands, and as far as we know, the semantics of this combination is unclear. This is exemplified in the "real hotel", a pendant of Hilbert's hotel, but now with an uncountable number of rooms. The question is how we should calculate the probability that the light on the hotel will switch on. Or more in general, how can we combine infinite choice and probability density functions in process algebras in a semantically sound manner.

Dave Parker – University of Birmingham

Invited Speaker for the Express/SOS workshop
Monday August 23, 2021, 13:00–14:00 CEST

Probabilistic Verification of Concurrent Autonomous Systems

Abstract: Modern computing systems increasingly involve autonomous agents acting concurrently, which may either compete or collaborate to achieve their own objectives. Designing these systems is a challenge, particularly when they need to operate in uncertain or adversarial environments. Probabilistic model checking is a technique for formal modelling and analysis of such systems. Given a quantitative correctness specification expressed in temporal logic, it can either verify that the system behaves as intended, or synthesise a controller which guarantees that this will be the case.
This tutorial explains some of the recent advances in this area, with a particular focus on the use of stochastic games to verify multi-agent systems. This includes concurrent stochastic games, for more realistic modelling of agents acting concurrently, and Nash equilibria, for more expressive specification of agents with differing objectives. We summarise the key underlying theory and algorithms, and illustrate the applicability of the techniques with examples from a range of applications.

Amal Ahmed – Northeastern University, Boston

Invited Speaker for the Express/SOS workshop
Monday August 23, 2021, 15:30–16:30 CEST

Semantic soundness for language interoperability

Abstract: Programs are rarely implemented in a single language, and thus questions of type soundness should address not only the semantics of a single language, but how it interacts with others. Even between type-safe languages, disparate typing features make interoperability fraught since type-based guarantees from one language may be easily be violated in the other. In their seminal 2007 paper, Matthews and Findler proposed a technique for modeling multi-language systems by augmenting interoperating languages with a pair of "boundaries" that allow code from the first language to be used in contexts of the second, and vice versa. While this technique has been widely applied, their source-to-source interoperability model doesn't reflect how multi-language systems are implemented in the wild, where terms only interact after compilation to a common target and safety must be mediated by target-level "glue code."
In this talk, I will describe a novel framework for proving type soundness of multi-language systems that follows an interoperation-after-compilation strategy. Language designers specify what types of data may be converted between the two languages and provide the target-level glue code that implements these conversions. We establish soundness of the conversions by giving a model of source-language types as sets of target-language terms, which in turn allows us to prove soundness of the multi-language. I will demonstrate this idea via several case studies, and illustrate how the approach helps designers identify more efficient safety-enforcement mechanisms, as well as opportunities for safe sharing of data.

Stanley Bak – Stony Brook University

Invited Speaker for the SNR workshop
Monday August 23, 2021, 14:00–14:45 CEST

Symbolic and Numeric Challenges in Neural Network Verification Methods

Abstract: The field of formal verification has traditionally looked at proving properties about finite state machines or software programs. Recent research has also looked at other classes of systems such as CPS models given with differential equations, or even systems that include neural networks. We present verification methods and symbolic and numerical challenges and optimizations that make scalable analysis increasingly practical.

Bardh Hoxha – Toyota Research Institute North America

Invited Speaker for the SNR workshop
Monday August 23, 2021, 15:45–16:30 CEST

Autonomous CPS: Verification and Control

Abstract: As Cyber-Physical Systems are becoming more autonomous, there is an increasing need for methods that ensure safety and reliability. In this talk, we present requirements-based approaches that can be used for automated testing, monitoring, and control synthesis of CPS. The methods utilize ideas from three important areas in CPS research: formal methods, machine learning, and control theory. We illustrate our methods on problems from the automotive industry.

Nils Jansen – Radboud University Nijmegen

Invited Speaker for the SNR workshop
Monday August 23, 2021, 17:00–17:45 CEST

Safe Planning under Epistemic Uncertainty and Partial Information

Abstract: This talk concerns planning problems that are subject to various sources of uncertainty. For example, an autonomous agent may operate under perceptual limitations due to imperfect knowledge about the accuracy of its sensors. To capture such problems with a formal model, we extend partially observable Markov decision processes (POMDPs) to account for epistemic uncertainty. The resulting uncertain POMDPs reflect uncertainty via uncountable sets of probability distributions caused by, for instance, a lack of data available. We present a novel method to compute finite-memory policies for uncertain POMDPs that robustly satisfy temporal logic specifications. In general, computing such policies is theoretically and practically intractable. Our solution is based on efficient convexification techniques for the underlying non-convex optimization problem. We demonstrate the applicability using examples from aircraft collision-avoidance and spacecraft motion planning.

Christel Baier – Technische Universität Dresden

Invited Speaker for the Trends workshop
Saturday August 28, 2021, 14:15–15:15 CEST

From verification to causality-based explications

Abstract: The early success story of the model checking approach relies fundamentally on two features. First, the algorithms provide a push-button technology: As soon as the model and specification have been generated, one obtains a result in a fully automated way. Second, if the algorithm terminates with a negative result, then it can infer counterexamples to the specification. Counterexamples are the first instances for what we use the term explication, which refers to a mathematical concept that in some way sheds light on why the model checker has returned the result. While counterexamples are single instances of execution traces violating the specification, they provide little insights in what causes the specification violation. To enhance the system transparency, more crisp explications for the satisfaction or violation of properties are demanded. The talk presents an overview of techniques that go in this direction by using formal notions of causality and responsibility to explicate verification results.

Alexey Gotsman – IMDEA Software Institute

Invited Speaker for the Trends workshop
Saturday August 28, 2021, 15:45–16:45 CEST

Rigorous Design of Atomic Transaction Commit Protocols

Abstract: Modern data stores often need to provide both high scalability and strong transactional semantics. They achieve scalability by partitioning data into shards and fault tolerance by replicating each shard across several servers. A key component of such systems is the protocol for atomically committing a transaction spanning multiple shards. Unfortunately, existing data stores entangle atomic commit protocols with the rest of the system and lack proofs of their correctness. On the other hand, the classical theory of atomic commit is too restrictive to capture the complexities of modern protocols. To fill this gap, I will present a new problem statement for atomic commit that more faithfully reflects modern requirements and will describe an efficient and provably correct solution to this problem. I will also explain how these results enable more modular and rigorous design of transactional data stores.

Ilaria Castellani – INRIA

Invited Speaker for the Trends workshop
Saturday August 28, 2021, 17:00–18:00 CEST

Event structure semantics for asynchronous multiparty sessions

Abstract: Session types have been an active trend of research for more than two decades. They are associated with session calculi, which are process calculi tailored to describe structured interactions among two or more parties. The aim of session types is to specify the structure of process interaction and to ensure classical properties of this interaction, such as deadlock-freedom.
Session calculi are usually given an operational semantics by means of an LTS or a reduction relation. In recent work with Mariangiola Dezani and Paola Giannini, we proposed a denotational semantics by means of Event Structures (ESs) for a core multiparty session calculus. We considered both synchronous and asynchronous communication: in both cases we defined an interpretation of multiparty sessions as Flow ESs and an interpretation of their types (when defined) as Prime ESs. The latter requires the causality relation to be extracted from an equivalence class of traces, since types are sequential specifications. We showed that when a session is typable, its Flow ES and the Prime ES of its type yield isomorphic domains of configurations.
In the talk I will focus on the asynchronous case, which is more novel in two respects: we provide an ES semantics for an asynchronous calculus, and we introduce new types for asynchronous multiparty sessions, which we call asynchronous types. Our new typing is more permissive than the original typing for asynchronous sessions, while remaining decidable.