KeynotesSTAF 2023

We are excited to announce five invited speakers from across the STAF’23 conferences (ECMFA, ICGT, and TAP):

TAP’23: Kim G. Larsen, Aalborg University (Denmark)

Symbolic, Statistical and Randomized Engines in UPPAAL

Tuesday 11am, Oak

UPPAAL provides a tool-suite supporting model checking, performance analysis, testing, synthesis and learning for real-time systems. Based on the underlying modeling formalism of timed automata, significant effort has been put into development and implementation of efficient datastructures and algorithmic methods. By now these methods have resulted in a variety of symbolic, statistical and randomized engines.

In the talk I will present the three algorithmic methods and highlight their particular benefits individually and in combinations. This include: 1) Randomized methods are useful in early phases of development for fast discovery leaving the use of expensive symbolic verification to the end of development. 2) Combining randomized and statistical methods we have proposed a new falsification testing methodology that is aware of expected system usage and underlying risks associated with different faulty behaviors, allowing for a ranking of counterexamples based on their expected impact. 3) UPPAAL Stratego combines symbolic and statistical (learning) methods for constructing safe and near-optimal control strategies.

We shall also report on current effort made towards a hierarchical modelling formalism, where first prototypes are being obtained using model transformations to the existing non-hierarchical formalism.

Finally during the talk we will provide on-line demo of the new release UPPAAL 5.0.

ICGT’23: Dan Ghica, Huawei Research and University of Birmingham (UK)

Syntactic trinitarianism: terms, graphs, diagrams

Wednesday 9am, Oak

The concept of ‘syntax’ is commonly understood as the structure hidden in linear sequences of tokens, which in language and logic we commonly call ‘terms’. However, for the purpose of analysis and transformation, compilers use more efficient data structures to represent syntax, namely graphs. The gap between the linear (term) and graph syntax is elegantly bridged by a third formalism, namely that of string diagrams, a planar representation of terms in the categorical representation of syntax. In this tutorial talk I will show how the interplay of terms, graphs, and diagrams can help specify and implement complex analyses and transformations in compilers for higher-order programming languages, such as type inference, automatic differentiation, or closure conversion. This methodology is at the foundation of a new industrial-strength compiler being implemented currently at Huawei.

Most of the material I will discuss is based on the recent tutorial paper “Hierarchical string diagrams and applications” jointly with Fabio Zanasi (https://arxiv.org/abs/2305.18945).

TAP’23: Mattias Ulbrich, Karlsruhe Institute of Technology (Germany)

KeY: A Verification Platform For Java

Wednesday 1:30pm, Willow

In recent years and decades, the research community has unleashed a diverse variety of approaches to formally assess and establish the correctness of programs on the source code level. It is still an active research area how the results of different verification techniques can be brought together profitably.

In this talk, I will present how the verification ecosystem surrounding the KeY tool allows one to combine a number of successful approaches. At its core, KeY is a deductive verification engine for the formal analysis of Java programs annotated with formal specifications written in the Java Modeling Language. It employs a dynamic logic calculus for Java driven by symbolic execution. We will learn about the working principles of this verification method and see how it was used to prove (or disprove) the correctness of relevant real-world Java components, for instance from the JDK.

In addition, I will present the Karlsruhe Java Verification Suite (KaJaVe), where we enriched the KeY prover infrastructure by a number of approaches that leverage other verification principles such that they can be used in combination with the deductive verifier.

ICGT’23: Mohammad Abdulaziz, King’s College London (UK)

Formal Mathematics: Matching Algorithms as a Case Study

Thursday 1:30pm, Willow

A formal proof is a proof within an axiomatic system, where proof steps are either applications of axioms or applications of formally proven statements. Formal proofs have a long history within mathematics, starting with Euclid’s element’s which had an axiomatic system for geometrical reasoning. The main motivation of constructing a formal proof is obtaining unambiguous detailed proofs that can be mechanically checked. The advent of computer-based tools for formal proof, such as automatic and interactive theorem provers, made it feasible to produce formal versions of proofs that would otherwise be impossible.

A matching in an undirected graph is a subset of the edges of the graph s.t. no two edges are incident on the same vertex. In addition to the rich mathematical structure exhibited by matchings, algorithms to compute matchings have many applications, ranging from matching kidney donors and recipients to the allocation of advertisers to users of search engines.

In this talk, after giving an overview of the state-of-the-art, I will discuss my work on applying formal proof technology to matching theory, discussing some interesting findings and the even more interesting open questions.

Biography. Mohammad Abdulaziz is a lecturer (equiv. to assistant professor) and member of the Reasoning and Planning Group at King’s College London. Before that, he was a post-doc in the Chair for Logic and Verification at Technische Universität München. His main research is in the area of formal mathematics, with a special focus on formalising theoretical CS, and the formal verification of algorithms and software.

ECMFA’23: Andrzej Wąsowski, IT University of Copenhagen (Denmark)

How I lost my faith (in language technology research)? There and back again.

Friday 9am, Oak

Modeling and language engineering have hardly ever been as successful as today. Whatever software domain you zoom into, you will find plenty external and internal modeling languages. Everybody is doing (multi-)modeling all the time. At the same time modeling has never been as invisible as it is today. Modeling is not a buzzword. Being a modeling-expert means not much, when everybody is a modeling expert.

In this talk, I will zoom in into two groups of modeling languages: reactive programming languages including behavior trees and state machines (as used in robotics) and probabilistic programming languages (as used in data science). While looking at these examples closely, I want to answer three questions: Concretely how and by whom are these modeling languages engineered? Why and how should people be taught language engineering in 2023? And, finally, how can one be a modeling researcher in 2023?