44th International Symposium on Mathematical Foundations of Computer Science August 2630, 2019, Aachen (Germany) 
MFCS 2019 is organized in cooperation with EATCS 
Invited SpeakersJé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 modelchecking 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 upperbound and improved the best known lowerbound of the reachability problem for vector addition systems, a 40 years old open problem. Talk: Petri Net Reachability ProblemAbstract: 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 (20102012) as a Simons Postdoctoral Fellow at University of California at San Diego, six years (20122018) 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 coauthor of the recent Parameterized Algorithms book. Talk: Picking Random VerticesAbstract: 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 stateoftheart parameterized, exact exponential time, and approximation algorithms for a number of problems, such as Feedback Vertex Set and 3Hitting Set. We will also discuss a recent 2approximation 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 (MaxPlanckInstitut 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 coauthored 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 PhDstudents 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 cofounder of Algorithmic Solutions Software GmbH. Talk: Trustworthy Graph AlgorithmsAbstract: The goal of the LEDA project was to build an easytouse 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 blossomshrinking 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 postdoc 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 TimeAbstract: 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 predicateguarded 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 PSPACEcomplete, 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, mincuts and GomoryHu trees, and minimum cycle basis algorithms. She did her PhD from TIFR Mumbai and was a postdoctoral researcher at MaxPlanckInstitut 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 MixedAbstract: 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 wellstudied model in twosided matching markets. A matching M is popular if it does not lose a headtohead 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 minsize popular matching and there are also simple linear time algorithms for computing a maxsize 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 NPhardness results for many popular matching problems. These include the mincost/maxweight popular matching problem and the problem of deciding if G admits a popular matching that is neither a minsize nor a maxsize popular matching. For nonbipartite graphs, it is NPhard 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 headtohead election against any mixed matching. As an allocation mechanism, a popular mixed matching has several nice properties. Moreover, finding a maxweight or mincost 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 nonbipartite graphs as well and can be computed in polynomial time.  
Important Dates

Contact: Peter Rossmanith mfcs2019@cs.rwthaachen.de Privacy Policy 