45th International Symposium on
Mathematical Foundations of Computer Science
August 24-28, 2020, Prague (Czech Republic)
MFCS 2020 is organized in cooperation with EATCS
ScheduleAll times are quoted in UTC+2 (Prague time).
All sessions except for Gather.town will be available via Zoom. Gather.town sessions will be available through web browsers and do not need any special software installed. Registered participants will receive access information via email on Friday, August 21.
Q/A Sessions will run as three parallel sessions. Each paper has assigned 10 minute slot, where we expect the authors to have a 5-7 minute presentation and the rest of the time will be available for questions. We ask all presenting authors to join their sessions via Zoom at least 10-15 minutes before the actual start of the session. They will run their presentation on their computer and share it via Zoom "Share screen" feature once requested by the session chair. To facilitate further questions to the authors after each session we ask the authors of each paper from a given session to attend the Gather.town break where their papers will have designated clearly marked spots/locations. Attendees interested in asking questions to the authors can locate the corresponding spot in the Gather.town and start audio/video conversation with the present authors.
We suggest to all presenting authors to use a good internet connection (preferably wired) and use a local installation of Zoom (which is free to install.).
Gather.town will be available continuously between 12:30 and 20:30 on each day.
Sergio Cabello (Ljubljana)Session chair(s): Dan Kral
TUE 13:00-13:50 UTC+2
Some Open Problems in Computational Geometry
We shall encounter three open problems in Computational Geometry that are, in my opinion, interesting for a general audience interested in algorithms.
Parthasarathy Madhusudan (UIUC)Session chair(s): Naoki Kobayashi
TUE 15:30-16:20 UTC+2
First-Order Logics with Recursive Definitions for Program Verification
We argue that first order logic with recursive definitions augmented with background theories forms an interesting, expressive, and largely automatable logic for formal verification of programs that manipulate datastructures. We will survey several recent results: (a) a heuristic technique called natural proofs that works well in practice and, theoretically, gives complete reasoning for certain FO logics with background theories, (b) a first order logic extended with frames that provides frame reasoning to ease proofs, and (c) techniques for tackling recursive definitions, which call for reasoning with least fixpoints, by divining hypotheses for inductive proofs using program/expression synthesis. These techniques are mainly evaluated in verification frameworks for programs that manipulate datastructures.
Mary Wootters (Stanford)Session chair(s): Standa Živný
TUE 18:00-18:50 UTC+2
List-Decodability of Structured Ensembles of Codes
What combinatorial properties are satisfied by a random subspace over a finite field? For example, is it likely that not too many points lie in any Hamming ball? What about any cube? In this talk, I will discuss the answer to these questions, along with a more general characterization of the properties that are likely to be satisfied by a random subspace. The motivation for this characterization comes from error correcting codes. I will discuss how to use this characterization to make progress on the questions of list-decoding and list-recovery for random linear codes, and also to establish the list-decodability of random Low Density Parity-Check (LDPC) codes.
This talk is based on the joint works with Venkatesan Guruswami, Ray Li, Jonathan Mosheiff, Nicolas Resch, Noga Ron-Zewi, and Shashwat Silas.
Subhash Khot (NYU)Session chair(s): László Végh
WED 13:00-13:50 UTC+2
Hardness of Approximation: From the PCP Theorem to the 2-to-2 Games Theorems
Computer scientists firmly believe that no algorithm can efficiently compute optimal solutions to a class of problems called NP-hard problems. For many NP-hard problems, even computing an approximately optimal solution remains NP-hard. This phenomenon, known as the hardness of approximation, has numerous connections to proof checking, optimization, combinatorics , discrete Fourier analysis, and geometry.
The talk will provide an overview of these connections. It will address why graph coloring is a computationally hard problem, how it is possible to check a proof without even looking at it, why computer scientists love the majority vote, and whether a shape exists that looks spherical as well as cubical. It will explain how all this fits into a 30-year research program starting with the foundational Probabilistically Checkable Proofs (PCP) Theorem and leading to the recent 2-to-2 Games Theorem.
Nathalie Bertrand (INRIA, Rennes)Session chair(s): Javier Esparza
WED 15:30-16:20 UTC+2
Concurrent Games with Arbitrarily Many Playerss
Traditional concurrent games on graphs involve a fixed number of players, who take decisions simultaneously, determining the next state of the game. With Anirban Majumdar and Patricia Bouyer, we introduced a parameterized variant of concurrent games on graphs, where the parameter is precisely the number of players. Parameterized concurrent games are described by finite graphs, in which the transitions bear finite-word languages to describe the possible move combinations that lead from one vertex to another.
We report on results on two problems for such concurrent games with arbitrary many players.
To start with, we studied the problem of determining whether the first player, say Eve, has a strategy to ensure a reachability objective against any strategy profile of her opponents as a coalition. In particular Eve's strategy should be independent of the number of opponents she actually has. We establish the precise complexities of the problem for reachability objectives.
Second, we considered a synthesis problem, where one aims at designing a strategy for each of the (arbitrarily many) players so as to achieve a common objective. For safety objectives, we show that this kind of distributed synthesis problem is decidable.
Q/A Sessions 1
TUE 14:00-15:00 UTC+2
Q/A Session 1ASession chair(s): Artur Jez
Q/A Session 1BSession chair(s): Jakub Gajarský
Q/A Session 1CSession chair(s): Iddo Tzameret
Q/A Sessions 2
TUE 16:30-17:30 UTC+2
Q/A Session 2ASession chair(s): Dirk Nowotka
Q/A Session 2BSession chair(s): Lukasz Kowalik
Q/A Session 2CSession chair(s): Matthias Englert
Q/A Sessions 3
WED 14:00-15:00 UTC+2
Q/A Session 3ASession chair(s): Thomas Colcombet
Q/A Session 3BSession chair(s): Standa Živný
Q/A Session 3CSession chair(s): László Végh
Q/A Sessions 4
WED 16:30-17:20 UTC+2
Q/A Session 4ASession chair(s): Mickael Randour
Q/A Session 4BSession chair(s): Broňa Brejová
Q/A Session 4CSession chair(s): Matthew Hague
Q/A Sessions 5
WED 17:50-18:40 UTC+2
Q/A Session 5ASession chair(s): Michael Blondin
Q/A Session 5BSession chair(s): Lukasz Kowalik
Q/A Session 5CSession chair(s): Iddo Tzameret
Contact: Andreas Emil Feldmann firstname.lastname@example.org