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
CNRS - Centre National de la Recherche Scientifique : UMR 8548, Inria Paris-Rocquencourt, DI-ENS - Département d'informatique de l'École normale supérieure
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

https://hal.inria.fr/hal-00925999
Contributor : Antoine Miné <>
Submitted on : Wednesday, January 8, 2014 - 11:37:00 PM
Last modification on : Thursday, July 1, 2021 - 5:58:03 PM

Identifiers

  • HAL Id : hal-00925999, version 1

Collections

Citation

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

Share

Metrics

Record views

280