Vincent Laviron and Francesco Logozzo
We introduce SubPolyhedra (SubPoly), a new family of numerical abstract domains to infer and propagate linear inequalities. The key insight is that the reduced product of linear equalities and intervals produces powerful yet scalable analyses. Abstract domains in SubPoly are as expressive as Polyhedra, but they drop some of the deductive power to achieve scalability. The cost/precision ratio of abstract domains in the SubPoly family can be fine-tuned according to the precision one wants to retain at join points, and the algorithm used to infer the tighter bounds on intervals. We implemented SubPoly on the top of ClousotUnknown control sequence 'tt ', a generic abstract interpreter for .Net. ClousotUnknown control sequence 'tt ' with SubPoly analyzes very large and complex code bases in few minutes. SubPoly can efficiently capture linear inequalities among hundreds of variables, a result well beyond the state-of-the-art implementations of Polyhedra.
|Published in||International Journal on Software Tools for Technology Transfer (STTT)|
Vincent Laviron and Francesco Logozzo. Refining Abstract Interpretation-based Static Analyses with Hints, Springer Verlag, December 2009.
Francesco Logozzo and Vincent Laviron. SubPolyhedra: A (more) scalable approach to infer linear inequalities, Springer Verlag, January 2009.