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.
Conference DaySun 13 JanDisplayed time zone: Belfast change
11:00 - 12:30
|Static Analysis of Binary Code with Memory Indirections Using Polyhedra|
Clément Ballabriga, Julien Forget, Laure GonnordUniversity of Lyon & LIP, France, Giuseppe Lipari, Jordy RuizFile Attached
|Disjunctive Relational Abstract Interpretation for Interprocedural Program Analysis|
|Application of Abstract Interpretation to the Automotive Electronic Control System|