Laurent Mauborgne, Associate Professor, École Normale Supérieure, Paris, France
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.