Distinguishing paths

Event details
Date | 08.06.2011 |
Hour | 10:15 |
Speaker | Prof. David Monniaux, CNRS, Vérimag |
Location | |
Category | Conferences - Seminars |
Usual techniques in abstract interpretation apply "join" operations when control flows from several nodes. Unfortunately, these techniques introduce imprecision, resulting in not being able to prove desired properties. Modern SMT-solving techniques allow enumerating paths "on demand". We shall see how such path techniques may be combined with conventional polyhedral analysis, quantifier elimination, or with policy iteration, in order to obtain more precise invariants. This is joint work with Laure Gonnord (Université Lille I / LIFL) and Thomas Gawlitza (then CNRS / VERIMAG, now at INRIA). Prof. Monniaux's homepage
Practical information
- General public
- Free