Static analysis of numerical properties in the presence of pointers
type: Dataset
description: The fast and furious pace of change in computing technology has become an article of faith for many. The reliability of computer-based systems cru- cially depends on the correctness of its computing. Can man, who created the computer, be capable of preventing machine-made misfortune? The theory of static analysis strives to achieve this ambition. The analysis of numerical properties of programs has been an essential research topic for static analysis. These kinds of properties are commonly modeled and handled by the concept of numerical abstract domains. Unfor- tunately, lifting these domains to heap-manipulating programs is not obvious. On the other hand, points-to analyses have been intensively studied to an- alyze pointer behaviors and some scale to very large programs but without inferring any numerical properties. We propose a framework based on the theory of abstract interpretation that is able to combine existing numerical domains and points-to analyses in a modular way. The static numerical anal- ysis is prototyped using the SOOT framework for pointer analyses and the PPL library for numerical domains. The implementation is able to analyze large Java program within several minutes. The second part of this thesis consists of a theoretical study of the com- bination of the points-to analysis with another pointer analysis providing information called must-alias. Two pointer variables must alias at some pro- gram control point if they hold equal reference whenever the control point is reached. We have developed an algorithm of quadruple complexity that sharpens points-to analysis using must-alias information. The algorithm is proved correct following a semantics-based formalization and the concept of bisimulation borrowed from the game theory, model checking etc.
identifier: NNT: 2013REN1S060
issued: 2026-05-07T18:58:36.695765
language: en
modified: 2026-05-07T18:58:36.695771
contact point: Organization
  fn: CCSD
keyword: abstract-interpretation
keyword: analyse-de-pointeurs
keyword: analyse-statique
keyword: analysis-of-pointers
keyword: bisimulation
keyword: infoeu-reposemanticsdoctoralthesis
keyword: infoinfo-ohcomputer-science-csother-csoh
keyword: interpretation-abstraite
keyword: must-alias
keyword: numerical-properties
keyword: proprietes-numerique
keyword: static-analysis
keyword: theses
landing page: https://theses.hal.science/tel-00918593

Static analysis of numerical properties in the presence of pointers
type: Distribution
format: HTML
issued: 2026-05-07T18:58:36.704104
modified: 2026-05-07T18:58:36.683935
access URL: https://theses.hal.science/tel-00918593

test_moissonnage_selune
type: Agent