Seminar on Foundations of Computing
This research seminar provides a venue for presenting research results concerning algorithm design, discrete mathematics, formal methods, logic and related areas of theoretical computer science. The seminar is jointly organized by the research laboratories DIMEA, FORMELA, and LIVE. The seminar builds on the FMDSA seminar organized by the FORMELA laboratory in the past.
Time and place
The seminar takes place on Monday at 2PM term time in Room C417 in the building of the Faculty of Informatics on a (roughly) weekly schedule.
Fall 2023 – schedule overview
25 September | Filip Pokrývka (Masaryk University) | Sparse Graphs of Twin-width 2 Have Bounded Tree-width |
02 October | Ehsan Goharshady (IST Austria) | Non-Termination: Program Reversal and Invariant Generation |
9 October | Michael Anastos (IST Austria) | Robust Hamilotnicity in families of Dirac graphs |
16 October | Chloé Capon and Nicolas Lecomte (University of Mons) | TBA |
13 November | Jan Böker | TBA |
11 December | Hoang La | TBA |
Filip Pokrývka (Masaryk University): Sparse Graphs of Twin-width 2 Have Bounded Tree-width
Monday, September 25, 14:00, room C417
Twin-width is a structural width parameter introduced by Bonnet, Kim, Thomassé and Watrigant [FOCS 2020]. Very briefly, its essence is a gradual reduction (a contraction sequence) of the given graph down to a single vertex while maintaining limited difference of neighbourhoods of the vertices, and it can be seen as widely generalizing several other traditional structural parameters. Having such a sequence at hand allows to solve many otherwise hard problems efficiently. Our paper focuses on a comparison of twin-width to the more traditional tree-width on sparse graphs. Namely, we prove that if a graph G of twin-width at most 2 contains no K_t,t subgraph for some integer t, then the tree-width of G is bounded by a polynomial function of t. As a consequence, for any sparse graph class C we obtain a polynomial time algorithm which for any input graph G∈C either outputs a contraction sequence of width at most c (where c depends only on C), or correctly outputs that G has twin-width more than 2. On the other hand, we present an easy example of a graph class of twin-width 3 with unbounded tree-width, showing that our result cannot be extended to higher values of twin-width.
Joint work with Benjamin Bergougnoux, Jakub Gajarský, Grzegorz Guśpiel, Petr Hliněný, and Marek Sokołowski
Ehsan Goharshady(IST Austria): Non-Termination: Program Reversal and Invariant Generation
Monday, October 02, 14:00, room C417
Proving the non-termination of programs is a fundamental challenge in the field of program analysis and verification. While verifying that a program always terminates is crucial for safety and reliability, the complement, non-termination proving, can be equally important for detecting bugs and verifying security-critical and real-time systems. In this talk, we will explore an approach for non-termination proving of polynomial programs via invariant generation techniques and program reversal.
Past terms
Spring 2021: Special Seminar – part of Round the World Relay in Combinatorics, where a number of seminars and groups around the world were getting together. Each site hosted a talk, and everyone was welcome.
Fall 2020: ITI Online Seminar – a one-semester online venue for presenting current research in discrete mathematics and theoretical computer science in the Czech Republic.