IMDEA Software

IMDEA initiative

Home > Events > Invited Talks > 2009 > Disjunctions that Scale Up

Laurent Mauborgne

Monday, March 30, 2009

3:30pm Room 3307

Laurent Mauborgne, Associate Professor, École Normale Supérieure, Paris, France

Disjunctions that Scale Up

Abstract:

The main difficulty in abstract interpretation is to handle disjunctions: on one hand, keeping precise disjunctive informations is very costly, and on the other hand, approximating disjunctions is the main source of imprecision in abstractions. We propose on demand semantic disjunctions, where disjunctions are based on semantic properties such as some values of the reachable states or more complex properties of the traces of the program leading to these states. Such disjunctions allow for parametric refinements of existing analyses while keeping scalability. We discuss implementation issues and show the interest of such techniques in the ASTRÉE analyzer.