We introduce Subpolyhedra (SubPoly) a new numerical abstract domain to infer and propagate linear inequalities. Subpoly is as expressive as Polyhedra, but it drops some of the deductive power to achieve scalability. Subpoly is based on the insight that the reduced product of linear equalities and intervals produces powerful yet scalable analyses. Precision can be recovered using hints. Hints can be automatically generated or provided by the user in the form of annotations. We implemented Subpoly on the top of Clousot, a generic abstract interpreter for .Net. Clousot 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 state-of-the-art implementations of Polyhedra. © 2009 Springer Berlin Heidelberg.
CITATION STYLE
Laviron, V., & Logozzo, F. (2009). Subpolyhedra: A (More) scalable approach to infer linear inequalities. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5403 LNCS, pp. 229–244). https://doi.org/10.1007/978-3-540-93900-9_20
Mendeley helps you to discover research relevant for your work.