Skip to Main content Skip to Navigation
Conference papers

Fixpoint computation in the polyhedra abstract domain using convex and numerical analysis tools

Abstract : Polyhedra abstract domain is one of the most expressive and used abstract domains for the static analysis of programs. Together with Kleene algorithm, it computes precise yet costly program invariants. Widening operators speed up this computation and guarantee its termination, but they often induce a loss of precision, especially for numerical programs. In this article, we present a process to accelerate Kleene iteration with a good trade-off between precision and computation time. For that, we use two tools: convex analysis to express the convergence of convex sets using support functions, and numerical analysis to accelerate this convergence applying sequence transformations. We demonstrate the efficiency of our method on benchmarks.
Document type :
Conference papers
Complete list of metadatas

https://hal-cea.archives-ouvertes.fr/cea-01834985
Contributor : Léna Le Roy <>
Submitted on : Wednesday, July 11, 2018 - 10:02:38 AM
Last modification on : Monday, February 10, 2020 - 6:14:14 PM

Links full text

Identifiers

Collections

CEA | DRT | LIST

Citation

Y. Seladji, O. Bouissou. Fixpoint computation in the polyhedra abstract domain using convex and numerical analysis tools. Verification, Model Checking, and Abstract Interpretation. VMCAI 2013. Lecture Notes in Computer Science, Jan 2013, Rome, Italy. pp.149-168, ⟨10.1007/978-3-642-35873-9_11⟩. ⟨cea-01834985⟩

Share

Metrics

Record views

103