Skip to Main content Skip to Navigation
Master thesis

Implémentation du domaine asbtrait numérique TVPI pour APRON

Abdellatif Atki 1, 2 
2 ABSTRACTION - Abstract Interpretation and Static Analysis
DI-ENS - Département d'informatique - ENS Paris, Inria Paris-Rocquencourt, CNRS - Centre National de la Recherche Scientifique : UMR 8548
Abstract : This paper extends the work of Simon, King, and M. Howe and proposes an implementation of the relational numerical abstract domain TVPI (Two Variables Per Inequality) for the APRON library. This domain expresses invariants of the form ax + by ≤ c, for any a, b and c. The interest of this domain lies in its attractive cost/accuracy ratio due mainly to three points: (1) its convenient representation (2) the relatively low cost of its operations (3) the existence of effective geometric algorithms specific to the TVPI case. In the implementation, we had to deal with some issues that have not been addressed in detail in Simon, King, and Howe , and to make technical choices in order to achieve the theoretical running-time. We also had to make choices on how to approximate test and assignment operations (two basic operations in a static analyzer) when the number of variables in a linear expression is greater than two.
Document type :
Master thesis
Complete list of metadata
Contributor : Antoine Miné Connect in order to contact the contributor
Submitted on : Wednesday, January 8, 2014 - 11:37:00 PM
Last modification on : Thursday, March 17, 2022 - 10:08:35 AM


  • HAL Id : hal-00925999, version 1



Abdellatif Atki. Implémentation du domaine asbtrait numérique TVPI pour APRON. Performance et fiabilité [cs.PF]. 2013. ⟨hal-00925999⟩



Record views