Keynote Speakers


Clark Barrett, Stanford University
Title: Domain-Specific Reasoning with Satisfiability Modulo Theories
(joint with FM'21)


Kim Guldstrand Larsen, Aalborg University

Title: Synthesizing Correct and Optimal Control Programs using Model Checking and Machine Learning

Abstract: Ever since Alonzo Church, Computer Science has strived for efficient methods for deriving correct by construction control programs from high level specifications. Most recently, machine learning has made a big leap in this direction: now it is possible to learn highly optimal strategies for complex games, e.g. Go. However, as painfully witnessed by a number of incidents involving autonomous vehicles, machine learning comes with no guarantees of safety. This talk will present UPPAAL STRATEGO -- the most recent branch of the UPPAAL tool suit -- which combine symbolic model checking techniques with reinforcement learning in order to efficiently obtain near-optimal yet guaranteed safe strategies for Hybrid Automata based Markov Decision Processes. The talk describes the underlying modelling and specification formalism, the symbolic and learning algorithms, as well as demonstrate the tool, and the ongoing challenges pursued. At this point, the applications of UPPAAL STRATEGO include control urban water systems, traffic, energy-aware buildings and power-electronics.

Bio: Kim Guldstrand Larsen is a Professor of Computer Science at Aalborg University (AAU), since 1993. He received Honorary Doctorate from Uppsala University (1999), ENS Cachan (2007), International Chair at INRIA (2016) and Distinguished Professor at North-Eastern University, Shenyang, China (2018). His research interests cover modeling, verification, performance analysis of real-time and embedded systems with applications to concurrency theory, model checking and machine learning.
He is the prime investigator of the verification tool UPPAAL for which he received the CAV Award in 2013. Other prized received include Danish Citation Laureates Award, Thomson Scientific Award as the most cited Danish Computer Scientist in the period 1990-2004 (2005), Grundfos Prize (2016), Ridder af Dannebrog (2007). He is member of the Royal Danish Academy of Sciences and Letters, The Danish Academy of Technical Science, where he is Digital wiseman. Also, he is member of the Academia Europaea. In 2015 he received the prestigious ERC Advanced Grant (LASSO), and in 2021 he won the Villum Investigator Grant (S4OS). He has been PI and director of several large centers and initiatives including CISS (Center for Embedded Software systems, 2002-2008), MT-LAB (Villum-Kahn Rasmussen Center of Excellence, 2009-2013), IDEA4CPS (Danish-Chinese Research Center, 2011-2017), INFINIT National ICT Innovation Network, 2009-2020), DiCyPS (Innovation Fund Center, 2015-2021). Finally, he is co-founder of the companies UP4ALL (2000), ATS (2017) and VeriAal (2020).


Leslie Lamport, Microsoft,
Q/A Session Title: "If you're Not Writing a Program Don't Use a Programming Language"

Abstract: Leslie Lamport invites attendees of its Q/A session to watch his recorded talk entitled "If you're Not Writing a Program Don't Use a Programming Language" ; any attendee of the Q/A session should watch one of the two slightly different versions of that talk on video: One given at the National University of Singapore in January 2020 It's at [1] One given at the 2018 Heidelberg Laureate Forum in September at [2]

Bio: Dr. Lamport received a doctorate in mathematics from Brandeis University. An unlikely chain of events led to his current position as distinguished researcher at Microsoft.
Dr. Lamport's initial research in concurrent algorithms made him well-known as the author of LaTeX, a document formatting system for the ever-diminishing class of people who write instead of podcasting or making videos.
He has received five honorary doctorates from European universities, but has always returned home to California. This display of patriotism was rewarded with membership in the National Academy of Engineering, the National Academy of Sciences, and the American Academy of Arts and Sciences--as well as an honorary doctorate from Brandeis.
Dr. Lamport now annoys computer scientists and engineers by urging them to understand an algorithm or system before implementing it, and scares them by saying they should use mathematics. In a vain attempt to get him to talk about other things, the ACM gave him the 2013 Turing Award.