Monday, May 30, 2022

Orna Kupferman's Interview with Christel Baier, Holger Hermanns and Joost-Pieter Katoen, CONCUR 2022 ToT Award Recipients

I am delighted to post Orna Kupferman's interview with CONCUR 2022 Test-of-Time Award recipients Christel Baier, Holger Hermanns and Joost-Pieter Katoen.

Thanks to Christel, Holger and Joost-Pieter for their answers (labelled BHK in what follows) and to Orna (Q below) for conducting the interview. Enjoy and watch this space for upcoming interviews with the other award recipients!

Q: You receive the CONCUR Test-of-Time Award 2022 for your paper "Approximate symbolic model checking of continuous-time Markov chains," which appeared
at CONCUR 1998. In that article, you combine three different challenges: symbolic algorithms, real-time systems, and probabilistic systems. Could you briefly explain to our readers what the main challenge in such a combination is?

BHK: The main challenge is to provide a fixed-point characterization of time-bounded reachability probabilities: the probability to reach a given target state within a given deadline. Almost all works in the field up to 1999 treated discrete-time probabilistic models and focused on "just" reachability probabilities: what is the probability to eventually end up in a given target state? This can be characterized as a unique solution of a linear equation system. The question at stake was: how to incorporate a real-valued deadline d? The main insight was
to split the problem in staying a certain amount of time, x say, in the current state and using the remaining d-x time to reach the target from its successor state. This yields a Volterra integral equation system; indeed time-bounded reachability probabilities are unique solutions of such equation systems. In the CONCUR'99 paper we suggested to use symbolic data structures to do the numerical integration; later we found out that much more efficient techniques can be applied.

Q: Could you tell us how you started your collaboration on the award-winning paper? In particular, as the paper combines three different challenges, is it the case that each of you has brought to the research different expertise?

BHK: Christel and Joost-Pieter were both in Birmingham, where a meeting of a
collaboration project between German and British research groups on stochastic systems and process algebra took place. There the first ideas of model checking continuous-time Markov chains arose, especially for time-bounded reachability: with stochastic process algebras there were means to model CTMCs in a compositional manner, but verification was lacking. Back in Germany, Holger suggested to include a steady-state operator, the counterpart of transient properties that can be expressed using timed reachability probabilities. We then also developed the symbolic data structure to support the verification of the entire logic.

Q: Your contribution included a generalization of BDDs (binary decision diagrams) to MTDDs (multi-terminal decision diagrams), which allow both Boolean and real-valued variables. What do you think about the current state of symbolic algorithms, in particular the choice between SAT-based methods and methods that are based on decision diagrams?

BHK: BDD-based techniques entered probabilistic model checking in the mid 1990's for discrete-time models such as Markov chains. Our paper was one of the first, perhaps even the first, that proposed to use BDD structures for real-time stochastic processes. Nowadays, SAT, and in particular SMT-based techniques belong to the standard machinery in probabilistic model checking. SMT techniques are e.g., used in bisimulation minimization at the language level, counterexample generation, and parameter synthesis. This includes both linear as well as non-linear theories. BDD techniques are still used, mostly in combination with sparse representations, but it is fair to say that SMT is becoming more and more relevant.

Q: What are the research topics that you find most interesting right now? Is there any specific problem in your current field of interest that you'd like to see solved?

BHK: This depends a bit on whom you ask! Christel's recent work is about cause-effect reasoning and notions of responsibility in the verification context. This ties into the research interest of Holger who looks at the foundations of perspicuous software systems. This research is rooted in the observation that the explosion of opportunities for software-driven innovations comes with an implosion of human opportunities and capabilities to understand and control these innovations. Joost-Pieter focuses on pushing the borders of automation in weakest-precondition reasoning of probabilistic programs. This involves loop invariant synthesis, probabilistic termination proofs, the development of deductive verifiers, and so forth. Challenges are to come up with good techniques for synthesizing quantitative loop invariants, or even complete probabilistic programs.

Q: What advice would you give to a young researcher who is keen to start working on topics related to symbolic algorithms, real-time systems, and probabilistic systems?

BHK: Try to keep it smart and simple.

Friday, May 06, 2022

HALG 2022: Call for participation

I am posting this call for participation on behalf of Keren Censor-Hillel, PC chair for HALG 2022. I expect that many colleagues from the Track A community will attend that event and enjoy its mouth-watering scientific programme.


7th Highlights of Algorithms conference (HALG 2022)
The London School of Economics and Political Science, June 1-3, 2022

The Highlights of Algorithms conference is a forum for presenting the highlights of recent developments in algorithms and for discussing potential further advances in this area. The conference will provide a broad picture of the latest research in algorithms through a series of invited talks, as well as the possibility for all researchers and students to present their recent results through a series of short talks and poster presentations. Attending the Highlights of Algorithms conference will also be an opportunity for networking and meeting leading researchers in algorithms.

For local information, visa information, or information about registration, please contact Tugkan Batu—


A detailed schedule and a list of all accepted short contributions is available at


Early registration (by 20th May 2022)

Students: £100
Non-students: £150

Late registration (from 21st May 2022)
Students: £175
Non-students: £225

Registration includes the lunches provided, coffee breaks, and the conference reception.

There are some funds from conference sponsors to subsidise student registration fees. Students can apply for a fee waiver by sending an email to Enfale Farooq ( by 15th May 2022. Those students presenting a contributed talk will be given priority in allocation of these funds. The applicants will be notified of the outcome by 17th May 2022.


Survey speakers:

Amir Abboud (Weizmann Institute of Science) 
Julia Chuzhoy (Toyota Technological Institute at Chicago)
Martin Grohe (RWTH Aachen University)
Anna Karlin (University of Washington)
Richard Peng (Georgia Institute of Technology)
Thatchaphol Saranurak (University of Michigan)

Invited talks:

Peyman Afshani (Aarhus University)  
Soheil Behnezhad (Stanford University)  
Sayan Bhattacharya (University of Warwick)
Guy Blelloch (Carnegie Mellon University)
Greg Bodwin (University of Michigan)
Mahsa Eftekhari (University of California, Davis)
John Kallaugher (Sandia National Laboratories)
William Kuszmaul (Massachusetts Institute of Technology)
Jason Li (Carnegie Mellon University)
Joseph Mitchell (SUNY, Stony Brook)
Shay Moran (Technion)
Merav Parter (Weizmann Institute of Science)
Aviad Rubinstein (Stanford University)
Rahul Savani (University of Liverpool)
Mehtaab Sawhney (Massachusetts Institute of Technology)
Jakub Tetek (University of Copenhagen)
Vera Traub (ETH Zurich)
Jan Vondrak (Stanford University)
Yelena Yuditsky (Universit√© Libre de Bruxelles)