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 SeptemberFilip Pokrývka (Masaryk University)Sparse Graphs of Twin-width 2 Have Bounded Tree-width
02 OctoberEhsan Goharshady (IST Austria)Non-Termination: Program Reversal and Invariant Generation
9 OctoberMichael Anastos (IST Austria)Robust Hamilotnicity in families of Dirac graphs
16 OctoberChloé Capon and Nicolas Lecomte (University of Mons)TBA
13 NovemberJan BökerTBA
11 DecemberHoang LaTBA

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 2023

Fall 2022

Spring 2022

Fall 2021

Spring 2021: Special Seminarpart 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 Seminara one-semester online venue for presenting current research in discrete mathematics and theoretical computer science in the Czech Republic.

Spring 2020

Fall 2019

Spring 2019