# Difference between revisions of "Seminar"

Jump to navigation
Jump to search

(Radu, David) |
|||

Line 1: | Line 1: | ||

+ | ==Schedule== | ||

+ | * Tuesday, February 18, 2014: Radu Iosif, Safety Problems are NP-complete for Flat Integer Programs with Octagonal Loops (a tutorial on rigorous acceleration techniques) | ||

==Pool of available subjects== | ==Pool of available subjects== | ||

===David Monniaux=== | ===David Monniaux=== | ||

Line 5: | Line 7: | ||

===Radu Iosif=== | ===Radu Iosif=== | ||

− | |||

# Underapproximation of Procedure Summaries for Integer Programs + Polynomially Bounded Control Sets (higher-order acceleration or acceleration for recursive programs) | # 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) | # 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) |

## Revision as of 11:03, 17 February 2014

## Schedule

- Tuesday, February 18, 2014: Radu Iosif, Safety Problems are NP-complete for Flat Integer Programs with Octagonal Loops (a tutorial on rigorous acceleration techniques)

## 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

- 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)