Wednesday, April 27, 2011
Speaker: David Monniaux
Venue: TU Vienna
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.