Skip to Main content Skip to Navigation

Static Analysis of Numerical Programs: Constrained Affine Sets Abstract Domain

Khalil Ghorbal 1 
1 LMeASI - Laboratoire Modélisation et Analyse de Systèmes en Interaction
LIST (CEA) - Laboratoire d'Intégration des Systèmes et des Technologies : DRT/LIST
Abstract : We aim at proving automatically the correctness of numerical behavior of a program by inferring invariants on numerical variables. More precisely, we over-approximate in a sound manner the set of reached values. We use Abstract Interpretation-based Static Analysis as a generic framework to de ne and ap- proximate the semantics of a program in a uni ed manner. The semantics that describe the real behavior of the program (concrete semantics) is in general unde- cidable. Abstract interpretation o ers a way to abstract this concrete semantics to obtain a decidable semantics involving machine-expressible objects. We in- troduce a new affine forms-based abstract domain, called constrained affine sets, which extends and generalizes an already existing abstract domain introduced by Eric Goubault and Sylvie Putot. The expressiveness of such new domain is enhanced thanks to its ability to encode and propagate linear constraints among variables. We have implemented our new domain to experiment the precision and the efficiency of our approach and compare our results to the already existing abstract domains. The theoretical work as well as the implementation and the experiments have been the subject of two publications [CAV 2009, CAV 2010].
Complete list of metadata

Cited literature [88 references]  Display  Hide  Download
Contributor : Khalil Ghorbal Connect in order to contact the contributor
Submitted on : Monday, November 21, 2011 - 9:31:21 PM
Last modification on : Thursday, February 17, 2022 - 10:08:03 AM
Long-term archiving on: : Monday, December 5, 2016 - 12:35:25 AM


  • HAL Id : pastel-00643442, version 1



Khalil Ghorbal. Static Analysis of Numerical Programs: Constrained Affine Sets Abstract Domain. Symbolic Computation [cs.SC]. Ecole Polytechnique X, 2011. English. ⟨pastel-00643442⟩



Record views


Files downloads