Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
SubPolyhedra: A (more) scalable approach to infer linear inequalities

Francesco Logozzo and Vincent Laviron


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 effciently capture linear inequalities among hundreds of variables, a result well-beyond state-of-the-art implementations of Polyhedra


Publication typeInproceedings
Published inProceedings of the 10th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'09)
SeriesLectures Notes in Computer Science
PublisherSpringer Verlag

Newer versions

Vincent Laviron and Francesco Logozzo. SubPolyhedra: a family of numerical abstract domains for the (more) scalable inference of linear inequalities , International Journal on Software Tools for Technology Transfer (STTT) , Springer Verlag, June 2011.

Francesco Logozzo. Practical verification for the working programmer with CodeContracts and Abstract Interpretation - Invited Talk, Springer Verlag, January 2011.

> Publications > SubPolyhedra: A (more) scalable approach to infer linear inequalities