D-Con 2025

The D-Con was founded as a forum of German researchers on Concurrency Theory to meet, collaborate, and exchange ideas. One of its main tasks is to connect the younger researchers in the field. Therefore, the meeting consists of several talks mostly from younger scientists that can talk about their research agenda, new ideas on ongoing work, or recent research results. The programme is enhanced with talks and tutorials from experienced researchers as well as invited talks.

D-Con 2025 will take place March 06 and 07 at University of Augsburg (with the usual in-official dinner March 05).

Registration

To register please send an email to lukas.bartl@uni-a.de with name, address (we need a complete postal address for the invoice), e-mail-address, and affiliation for each participant. Please also tell us for each participant whether you want to attend the dinner on Wednesday March 05 and/or Thursday March 06. We will charge a fee of 50€ per participant to provide a snack during breaks. As ususal the two dinner are organised by us but have to be paid by yourself.

We welcome proposals for talks. We favour standard student talks (20min + questions and answers) but are open to other formats (talks by groups, tutorials, etc.). To propose a talk please send an email to lukas.bartl@uni-a.de.

Please send us your registration as well as talk proposals no later than February 07 2025.

Programme

Thursday, March 06

09:00	Invited Talk by Jorge A. Perez from the University of Groningen (https://www.jperez.nl/) Title: Comparing Deadlock-Free Typed Processes Abstract: As modern software systems rely on concurrency and distribution, ensuring the reliability of the message-passing programs that enable their operation is a critical concern. In this talk, the interest is in the deadlock freedom (DF) property for message-passing programs, which informally means that their processes "never get stuck''. DF is a most desirable property: in today's long-running infrastructures, even a single component that becomes permanently blocked while waiting for a message can severely impact system reliability and availability. Enforcing DF for message-passing programs can be challenging. The pi-calculus provides a firm and expressive basis for analysis techniques that can ensure deadlock freedom, with various type systems proposed for this purpose. In particular, type systems based on the Curry-Howard correspondence between session types and linear logic effectively enforce DF, and do so by following elegant proof-theoretical principles. This diversity of type systems raises the natural question of how the different proposals compare to each other. To tackle this question, in recent work we have formally compared different type systems for the pi-calculus that ensure (forms of) DF. I will introduce a few type systems and discuss the essential mechanisms that enable them to detect deadlocks. Then, I will overview our technical approach to establishing formal relationships between them and the classes of (deadlock-free) processes they induce.
10:00	Coffee Break
10:30	Talk by Benjamin Bisping from TU Berlin Title: Deciding All Behavioral Equivalences at Once through Energy Games Abstract: Concurrency theory has come up with a spectrum of behavioral equivalences for programs (e.g. bisimilarity, trace equivalence, ready traces), which vary in granularity. My recent approach turns the whole family of equivalence problems into one quantitative problem of “how” equivalent two models are. The core idea is to generalize the bisimulation game into a multi-dimensional energy game, where the attacker has to tell processes apart using limited resources. (Talk based on papers at CAV'23 and EXPRESS/SOS'24, joint work with David N. Jansen.)
11:00	Talk by Jens Gutsfeld from TU Braunschweig
11:30	Talk by Roman Lakenbrink from Universität Münster Title: Model Checking Dynamic Pushdown Networks with Locking Abstract: Dynamic Pushdown Networks (DPNs) are a model for multithreaded programs with recursion and dynamic creation of threads. In this talk, we enrich the model with a locking mechanismn allowing dynamic creation of locks. Each thread can reference a finite number of locks via local variables, create new locks, and overwrite its variables with new locks, either permanently or while being inside a procedure. Using tree automata techniques, we investigate the model checking problem for this model against properties that can be expressed by tree automata.
12:00	Talk by Lara Bargmann from Carl von Ossietzky Universität Oldenburg Title: Unifying Weak Memory Verification using Potentials Abstract: Concurrency verification for weak memory models is inherently complex. Several deductive techniques based on proof calculi have recently been developed, but these are typically tailored towards a single memory model through specialised assertions and associated proof rules. In this paper, we propose an extension to the logic Piccolo to generalise reasoning across different memory models. Piccolo is interpreted on the semantic domain of thread potentials. By deriving potentials from weak memory model states, we can define the validity of Piccolo formulae for multiple memory models. We moreover propose unified proof rules for verification on top of Piccolo. Once (a set of) such rules has been shown to be sound with respect to a memory model MM, all correctness proofs employing this rule set are valid for MM. We exemplify our approach on the memory models SC, TSO and SRA using the standard litmus tests Message-Passing and IRIW.
12:30	Lunch Break
13:30	Talk by Lukas Bartl from Universität Augsburg Title: Exploiting Instantiations from Paramodulation Proofs in Isabelle/HOL Abstract: Metis is an ordered paramodulation prover built into the Isabelle/HOL proof assistant. It attempts to close the current goal using a given list of lemmas. Typically these lemmas are found by Sledgehammer, a tool that integrates external automatic provers. We present a new tool that analyzes successful Metis proofs to derive variable instantiations. These increase Sledgehammer’s success rate, improve the speed of Sledgehammer-generated proofs, and help users understand why a goal follows from the lemmas.
14:00	Talk by Felix Stutz from the University of Luxembourg Title: An Automata-theoretic Basis for Specification and Type Checking of Multiparty Protocols Abstract: We present the Automata-based Multiparty Protocols framework (AMP) for top-down protocol development. The framework features a new very general formalism for global protocol specifications called Protocol State Machines (PSMs), Communicating State Machines (CSMs) as specifications for local participants, and a type system to check a π-calculus with session interleaving and delegation against the CSM specification. Moreover, we define a large class of PSMs, for which we provide a sound and complete PSPACE projection operation that computes a CSM describing the same protocol as a given PSM if one exists. We propose these components as a backwards-compatible new backend for frameworks in the style of Multiparty Session Types. In comparison to the latter, AMP offers a considerable improvement in expressivity, decoupling of the various components (e.g. projection and typing), and robustness (thanks to the complete projection). This talk is based on joint work with Emanuele D'Osualdo, to appear at ESOP25.
14:30	Talk by Sören van der Wall from TU Braunschweig Title: An automated rely-guarantee type system for Non-Interference in concurrent and speculating semantics Abstract: We aim for a type system that guarantees that secret values do not impact side-channel observations of programs under speculating, concurrent semantics. Formal side-channel security introduced semantics to make the side-channel leakages in programs visible, extended to speculating semantics upon the rise of Spectre attacks. The de-facto standard to avoid side-channel attacks is a non-interference property that ensures absence of secret dependent leakages. A recent attack demonstrated the possibility for synchronisation mechanisms to be bypassed by speculation. This calls for a concurrent, speculating semantics and a formalism to ensure program security. Previous works on Non-Interference for concurrent programs seem to focus on manual programming logics. We propose an automatically checkable type system that ensures non-interference for concurrent, speculating semantics. This is a "work in progress".
15:00	Talk by Emanuele D'Osualdo from Universität Konstanz Title: Bluebell: An Alliance of Relational Lifting and Independence For Probabilistic Reasoning Abstract: We present Bluebell, a program logic for reasoning about probabilistic programs where unary and relational styles of reasoning come together to create new reasoning tools. Unary-style reasoning is very expressive and is powered by foundational mechanisms to reason about probabilistic behaviour like independence and conditioning. The relational style of reasoning, on the other hand, naturally shines when the properties of interest compare the behaviour of similar programs (e.g. when proving differential privacy) managing to avoid having to characterize the output distributions of the individual programs. So far, the two styles of reasoning have largely remained separate in the many program logics designed for the deductive verification of probabilistic programs. In Bluebell, we unify these styles of reasoning through the introduction of a new modality called “joint conditioning” that can encode and illuminate the rich interaction between conditional independence and relational liftings; the two powerhouses from the two styles of reasoning.
15:30	Coffee Break
16:00	Talk by Karla Messing from Universität Duisburg-Essen Title: Galois Connections, Hennessy-Milner Theorems, and Witnesses Abstract: A Galois connection between a logical and a behavioural side allowed us to obtain Hennessy-Milner type theorems for different instantiations. We use this setting to find a "witness" for a threshold on the behavioural side: an element of the logical side which witnesses this threshold (if possible). In certain instantiations this corresponds to finding a formula that is not quite a distinguishing formula, but witnesses that there is a distance of more than a certain value between given states of a transition system. By adapting a general fixpoint game on complete lattices to this setting, we can use Spoilers strategy to find such a witness and vice versa.
16:30	Tutorial by Nadine Karsten from TU Berlin Title: ProofBuddy – A Teaching and Learning Platform for Proofs Abstract: Writing and checking proofs is difficult for students, but there is often too little time in lecture to teach competences needed. We developed the web application ProofBuddy based on the proof assistant Isabelle, which (1) helps students to write (mathematical) proofs in a structured way and (2) provides immediate feedback on completeness and correctness. The tutorial gives an introduction in ProofBuddy, shows the perspectives of teachers and learners and ends with some exercises within the platform.
19:00	Dinner

Friday, March 07

09:00	Talk by Caroline Lemke from Carl von Ossietzky Universität Oldenburg Title: Galois Energy Games to Solve Quantitative Reachability Problems Abstract: In studying reactive systems many questions can be reformulated by asking who wins a two-player game. When resource constraints have to be considered, (multi-weighted) energy games are utilized to represent (multiple) such quantitative goals. In this talk, we focus on the decidability of (multi-weighted) energy games with reachability winning conditions. In these zero-sum, two-player games, the goal is to navigate directed graphs labeled with energy functions, ensuring that a target is reached before running out of energy. However, efficiently solving these problems becomes difficult when multiple quantitative objectives are involved. We introduce a novel approach based on Galois connections to simplify checking the decidability of these games. By abstracting properties of energy functions, we define a new decidable class of games: Galois energy games. To rigorously demonstrate the validity of our results, we formalize the proof of decidability for a special case using the proof assistant Isabelle/HOL. In particular, we provide a machine-checked proof for the decidability of Bisping’s energy game, which is used to simultaneously decide all common notions of behavioral equivalence.
09:30	Talk by Jan Grünke from TU Braunschweig Title: Cyclic Proofs for Axiomatic Memory Models Abstract: We present an automated verification approach for axiomatic memory consistency models. It can prove properties of single memory models like the monotonicity of barriers, and also compare models like TSO and ARM8. To achieve this expressiveness, our approach has full support for intersections and converses of relations, and for constructing relations from Cartesian products of sets. At the heart of our approach is a cyclic proof system that is sound, complete, and optimal from a complexity point of view. We have implemented the proof search and exercised it on a number of benchmarks — with promising results.
10:00	Coffee Break
10:30	Talk by Lara Stoltenow from Universität Duisburg-Essen Title: Counterexample-Guided Abstraction Refinement for Graph Transformation Systems Abstract: Given a graph transformation system and starting from a certain class of initial graphs, can we guarantee (non-)reachability of a certain other class of graphs that characterizes bad or erroneous states? Both initial and bad states are characterized by nested conditions (having first-order expressive power). Such systems typically have an infinite state space, causing the problem to be undecidable. We use abstract interpretation to obtain a finite approximation of that state space, and use counter-example guided abstraction refinement to automatically (iteratively) obtain suitable predicates for verification.
11:00	Business Meeting and Lunch

Venue

We organise D-Con 2025 at the University of Augsburg in the building N (Universitätsstraße 6a, Campus location). Leave tram 3 at the station 'Universität'. Leaving the tram you are facing the building M (Mensa). Building N is next to M on the left of M. Turn left and walk until the path splits. Turn right and follow the path that goes between the buildings M and N. The buildings M and N are connected by a bridge on the first upper floor. The path brings you to a door into building N right under this bridge. In the building N turn right and go to the end of the building. The workshop is in the room 1058 N; registration and breaks are in room 1057 N.

Dinner March 05 will be indian food at Sangam at 19:00. The Sangam is in the city center; 15 min walking from the central station. Alternatively, you can take the tram (for free) from the central station to Königsplatz, then from Königsplatz to Moritzplatz and then walk the rest. In both cases you will pass by the Moritzplatz. There you will have to look straight ahead for stairs leading downwards between two buildings. Left of the stairs is a Stadtsparkasse and on the right is a large light green building hosting a restaurant called "Der König von Flandern im Kapitol". At the bottom of the stairs go to the next crossing and turn right. The restaurant is situated in the building on the right hand side of the street. The restaurant has vegan and gluten-free options. Reservation is on the name Peters.

Dinner March 06 will be local (Swabian and Bavarian) food at the "König of Flandern" at 19:00. The restaurant is at Moritzplatz (in a light green building see description above). The restaurant has vegan and gluten-free options. Reservation is on the name Peters.

Accommodation

There are a lot of hotels e.g. around the central station. In particular we can recommend the ibis Hotel Augsburg Hauptbahnhof at Halderstraße 25.

Travel Information

The tram line 3 goes from the central station of Augsburg via the Königsplatz to the University of Augsburg. The Königsplatz offers many conections to other trams and busses and marks the starting point of the pedestrian area into the city center.

Without the 'Deutschlandticket' the cheapest way to use the trams during D-Con is most likely the so-called AVV-Hotelticket Innenraum. This ticket is valid for 2 days (take Thursday and Friday) and allows you arbitrary many rides on busses and trams in the Zones 10 and 20, i.e., the inner part of Augsburg including the University. You can order the ticket at your hotel's reception desk.

Moreover, the trams in the city center are free of charge ( City-Zone). You can use this e.g. to get from the central station to the city center for the first dinner on Wednesday March 05.