Invited Speakers

Jérôme Leroux (LaBRI, Talence)

Jérôme Leroux is a CNRS senior researcher, head of the Formal Methods team of the computer science laboratory of Bordeaux (LaBRI) in France. He did his PhD under the supervision of Alain Finkel at the computer science laboratory of Cachan (LSV) in France on the model-checking of counter machines (defended in 2003). Over the past twenty years, he has been involved in several national and international research projects in the areas of the formal verification of infinite state systems, supported by several research grants from governmental research agencies. He worked on automata approaches for solving the Presburger arithmetic up to 2006 before starting his research project on the reachability problem for vector addition systems, also known as Petri nets, one of the central problem in theoretical computed science. In 2009 a provided a new approach for solving that problem based on Presburger inductive invariants. Very recently, in 2015 and 2018, he provided with his coauthors the very first complexity upper-bound and improved the best known lower-bound of the reachability problem for vector addition systems, a 40 years old open problem.

Talk: Petri Net Reachability Problem

Abstract: Petri nets, also known as vector addition systems, are a long established model of concurrency with extensive applications in modelling and analysis of hardware, software and database systems, as well as chemical, biological and business processes. The central algorithmic problem for Petri nets is reachability: whether from the given initial configuration there exists a sequence of valid execution steps that reaches the given final configuration. The complexity of the problem has remained unsettled since the 1960s, and it is one of the most prominent open questions in the theory of verification. In this presentation, we overview decidability and complexity results over the last fifty years about the Petri net reachability problem.

Daniel Lokshtanov (University of California at Santa Barbara (UCSB))

Daniel Lokshtanov received his PhD in Computer Science (2009), from the University of Bergen. Lokshtanov spent two years (2010-2012) as a Simons Postdoctoral Fellow at University of California at San Diego, six years (2012-2018) as a faculty member at the University of Bergen and is now an Associate Professor at the Department of Computer Science at the University of California Santa Barbara. His main research interests are in graph algorithms, parameterized algorithms and complexity. He is a co-author of the recent Parameterized Algorithms book.

Talk: Picking Random Vertices

Abstract: We survey some recent graph algorithms that are based on picking a vertex at random and declaring it to be a part of the solution. This simple idea has been deployed to obtain state-of-the-art parameterized, exact exponential time, and approximation algorithms for a number of problems, such as Feedback Vertex Set and 3-Hitting Set. We will also discuss a recent 2-approximation algorithm for Feedback Vertex Set in Tournaments that is based on picking a vertex at random and declaring it to /not/ be part of the solution.

Kurt Mehlhorn (Max-Planck-Institut für Informatik, Saarbrücken)

Kurt Mehlhorn is a Director of the MPI for Informatics and Professor of Computer Science at Saarland University. He heads the algorithms and complexity group at the MPI for Informatics. He works on data structures and algorithms in a broad sense. He co-authored some 300 publications in the field, published six books, and is one of the people behind the LEDA software library. He supervised more than 100 PhD-students and postdocs, many of whom have now faculty positions. He has received several prizes (Leibniz Award, Beckurts Award, Zuse Medal, Humboldt Award, EATCS Award, ACM Paris Kanellakis Theory and Practice Award, Erasmus Medal of the Academia Europaea) for his work. He holds Honorary Doctorate Degrees from Magdeburg, Waterloo, Aarhus, Gothenburg, and Patras universities and is an ACM Fellow. He is a member of the German Academy of Sciences Leopoldina, Academia Europaea, the German Academy of Science and Engineering acatech, the US Academy of Engineering, and the US Academy of Science. From 2002 to 2008, he was vice president of the Max Planck Society. He is a co-founder of Algorithmic Solutions Software GmbH.

Talk: Trustworthy Graph Algorithms

Abstract: The goal of the LEDA project was to build an easy-to-use and extendable library of correct and efficient data structures, graph algorithms and geometric algorithms. We report on the use of formal program verification to achieve an even higher level of trustworthiness. Specifically, we report on an ongoing and largely finished verification of the blossom-shrinking algorithm for maximum cardinality matching.

Alexandra Silva (University College London)

Alexandra Silva is a theoretical computer scientist whose main research focuses on semantics of programming languages and modular development of algorithms for computational models. A lot of her work uses the unifying perspective offered by coalgebra, a mathematical framework established in the last decades. Alexandra is currently a Professor of Algebra, Semantics, and Computation at University College London. Previously, she was an assistant professor in Nijmegen and a post-doc at Cornell University, with Prof. Dexter Kozen, and a PhD student at the Dutch national research center for Mathematics and Computer Science (CWI), under the supervision of Prof. Jan Rutten and Dr. Marcello Bonsangue. She was the recipient of the Needham Award 2018, the Presburger Award 2017, the Leverhulme prize 2016, and an ERC starting Grant in 2015.

Talk: Guarded Kleene Algebra with Tests: Verification of Uninterpreted Programs in Nearly Linear Time

Abstract: Guarded Kleene Algebra with Tests (GKAT) is a variation on Kleene Algebra with Tests (KAT) that arises by restricting the union (+) and iteration (*) operations from KAT to predicate-guarded versions. We develop the (co)algebraic theory of GKAT and show how it can be efficiently used to reason about imperative programs. In contrast to KAT, whose equational theory is PSPACE-complete, we show that the equational theory of GKAT is (almost) linear time. We also provide a full Kleene theorem and prove completeness for an analogue of Salomaa’s axiomatization of Kleene Algebra. We will also discuss how this result has practical implications in the verification of programs, with examples from network and probabilistic programming. This is joint work with Nate Foster, Justin Hsu, Tobias Kappe, Dexter Kozen, and Steffen Smolka.

Kavitha Telikepalli (Tata Institute of Fundamental Research, Mumbai)

Kavitha Telikepalli is an Associate Professor at the Tata Institute of Fundamental Research (TIFR), Mumbai. She works in combinatorial optimization and efficient graph algorithms. She has worked on matchings under preferences, spanners and related problems on approximate distances, min-cuts and Gomory-Hu trees, and minimum cycle basis algorithms. She did her PhD from TIFR Mumbai and was a post-doctoral researcher at Max-Planck-Institut für Informatik, Saarbrücken. She was an Assistant Professor at Indian Institute of Science, Bangalore before joining the faculty of TIFR Mumbai. She is currently an Associate Editor of ACM Transactions on Algorithms.

Talk: Popular Matchings: Good, Bad, and Mixed

Abstract: We consider the landscape of popular matchings in a bipartite graph G where every vertex has strict preferences over its neighbors. This is a very well-studied model in two-sided matching markets. A matching M is popular if it does not lose a head-to-head election against any matching, where each vertex casts a vote for the matching where it gets a better assignment. Roughly speaking, a popular matching is one such that there is no matching where more vertices are happier. The notion of popularity is more relaxed than stability: a classical notion studied for the last several decades. Popular matchings always exist in G since stable matchings always exist in a bipartite graph and every stable matching is popular. Algorithmically speaking, the landscape of popular matching seems to have only a few bright spots. Every stable matching is a min-size popular matching and there are also simple linear time algorithms for computing a max-size popular matching and for the popular edge problem. All these algorithms reduce the popular matching problem to an appropriate question in stable matchings and solve the corresponding stable matching problem. We now know NP-hardness results for many popular matching problems. These include the min-cost/max-weight popular matching problem and the problem of deciding if G admits a popular matching that is neither a min-size nor a max-size popular matching. For non-bipartite graphs, it is NP-hard to even decide if a popular matching exists or not. A mixed matching is a probability distribution or a lottery over matchings. A popular mixed matching is one that never loses a head-to-head election against any mixed matching. As an allocation mechanism, a popular mixed matching has several nice properties. Moreover, finding a max-weight or min-cost popular mixed matching in G is easy (by solving a linear program). Interestingly, there is always an optimal popular mixed matching p with a simple structure: p = {(M_0,1/2),(M_1,1/2)} where M_0 and M_1 are matchings in G. Popular mixed matchings always exist in non-bipartite graphs as well and can be computed in polynomial time.

Contact: Peter Rossmanith mfcs2019@cs.rwth-aachen.de Privacy Policy