Lies Lakhdar-Chaouch, Bertrand Jeannet, Alain Girault. Widening with Thresholds for Programs with Complex Control Graphs. Rapport de recherche INRIA, No 0, July 2011.
Download paper:
Adobe portable document (pdf)
Copyright notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.
{The precision of an analysis based on abstract interpretation does not only depend on the expressiveness of the abstract domain, but also on the way fixpoint equations are solved: exact solving is often not possible. The traditional solution is to solve iteratively abstract fixpoint equations, using extrapolation with a widening operator to make the iterations converge. Unfortunately, the extrapolation too often loses crucial information for the analysis goal. A classical technique for improving the precision is ''widening with thresholds'', which bounds the extrapolation. Its benefit strongly depends on the choice of relevant thresholds. In this paper we propose a semantic-based technique for automatically inferring such thresholds, which applies to any control graph, be it intraprocedural, interprocedural or concurrent, without specific assumptions on the abstract domain. Despite its technical simplicity, our technique is able to infer the relevant thresholds in many practical cases.}
[ Static analysis ] [ Abstract interpretation ] [ Numerical and symbolic abstract domains ] [ Convex polyhedra ] [ Semantic equation solving ] [ Widening ]
Bertrand Jeannet http://pop-art.inrialpes.fr/people/bjeannet/
Alain Girault http://pop-art.inrialpes.fr/people/girault/
@TechReport{LIES:2011:INRIA-00606961:1,
Author = {Lakhdar-Chaouch, Lies and Jeannet, Bertrand and Girault, Alain},
Title = {Widening with Thresholds for Programs with Complex Control Graphs},
Number = {0},
Pages = {0--0},
Institution = {INRIA},
Month = {July},
Year = {2011}
}
Get EndNote Reference (.ref)