Disjunctive Relational Abstract Interpretation for Interprocedural Program Analysis
Program analysis by abstract interpretation using relational abstract domains — like polyhedra or octagons — easily extends from state analysis (construction of reachable states) to relational analysis (construction of input-output relations). In this paper, we exploit this extension to enable interprocedural program analysis, by constructing relational summaries of procedures. In order to improve the accuracy of procedure summaries, we propose a method to refine them into disjunctions of relations, these disjunctions being directed by preconditions on input parameters.
Sun 13 Jan
|11:00 - 11:30|
Clément Ballabriga, Julien Forget, Laure GonnordUniversity of Lyon & LIP, France, Giuseppe Lipari, Jordy RuizFile Attached
|11:30 - 12:00|
|12:00 - 12:30|