POPL 2019 (series) / VMCAI 2019 (series) / VMCAI 2019 - 20th International Conference on Verification, Model Checking, and Abstract Interpretation /
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.
Slides (main.pdf) | 278KiB |
Sun 13 JanDisplayed time zone: Belfast change
Sun 13 Jan
Displayed time zone: Belfast change
11:00 - 12:30 | |||
11:00 30mTalk | Static Analysis of Binary Code with Memory Indirections Using Polyhedra VMCAI Clément Ballabriga , Julien Forget , Laure Gonnord University of Lyon & LIP, France, Giuseppe Lipari , Jordy Ruiz File Attached | ||
11:30 30mTalk | Disjunctive Relational Abstract Interpretation for Interprocedural Program Analysis VMCAI File Attached | ||
12:00 30mTalk | Application of Abstract Interpretation to the Automotive Electronic Control System VMCAI |