List DILS vous invite à son événement
À propos de cet événement
Numerical program analysis by abstract interpretation depends on how the target program is written. To gain precision, and ensure analysis robustness, it can be interesting to transform program before analyzing them. My thesis focuses on transformations to a form that is easier to analyze: static single assignment (SSA), as well as on analyses that exploit SSA properties.
First, I've developed a technique to transform programs inside an abstract interpreter. This allows performing the analysis and the transformations simultaneously, which leads to mutual improvements. Applying it to SSA transformations yields more precise numerical analysis, as it enables reasoning on the program values rather than its variables and allows for more constraint propagations than a standard numeric domain.
Next, I introduced a fast relational domain based on union-find, which benefits from SSA immutability. It can represent binary injective relation between terms, such as y=ax+b, and factorize other domains, reducing the number of SSA terms they need to handle. Finally, I've extended this domain to store flow-sensitive information by defining a fast join and inclusion check on union-find.
Proposé par
Le CEA est un organisme de recherche sur la défense et la sécurité, les énergies nucléaire et renouvelables, la recherche technologique pour l’industrie et la recherche fondamentale en sciences de la matière et de la vie.
