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

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.