Disjunctions that Scale Up

March 30, 2009

Laurent Mauborgne


Disjunctions that Scale Up

Time:   3:30pm
Location:   Room 3307

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.