Relational summaries for interprocedural analysis
Speaker(s) : Remy Boutonnet (VERIMAG)
Linear Relation Analysis, or polyhedral abstract interpretation, is able to discover automatically sets of linear relations between program variables at each program point. Despite being invented a long time ago, it is still one of the most powerful existing relational analyses. However its high complexity in the number of variables hinders its scalability to large monolithic programs. The structure of programs, as collections of procedures, classes or even modules, hints towards the long story of interprocedural analysis, especially bottom-up analyses, in which procedures are analyzed only once, by computing procedure summaries. We designed a new modular analysis, which computes disjunctive relational procedure summaries, to improve the scalability of Linear Relation Analysis. Our approach extends naturally to programs with recursive procedures and we are now interested in computing summaries of components in synchronous languages such as Lustre and methods in object-oriented languages.