# Seminar

## Pool of available subjects

### David Monniaux

- (or Julien Henry) Worst-case execution time analysis of programs using SMT and a clever encoding
- Single-cell abstraction of arrays

### Radu Iosif

- Safety Problems are NP-complete for Flat Integer Programs with Octagonal Loops (a tutorial on rigorous acceleration techniques)
- Underapproximation of Procedure Summaries for Integer Programs + Polynomially Bounded Control Sets (higher-order acceleration or acceleration for recursive programs)
- The Tree Width of Separation Logic with Recursive Definitions + Deciding Entailments in Inductive Separation Logic with Tree Automata (a tutorial on Separation Logic for compositional program analysis with emphasis on decidability issues)