Abstract acceleration in Linear relation analysis

{Linear Relation Analysis~\cite{cousot78,halbwach79} is now a classical abstract interpretation based on an approximation of reachable numerical states of a program by convex polyhedra. Since it works with a lattice of infinite depth, it makes use of a widening operator to enforce the convergence of fixpoint computations. This paper takes place in the many attempts to improve the precision of the results reached using such a widening. It will first present an extended survey of the existing approaches in that direction. Then it will investigate the cases where the exact (abstract) effect of a loop can be computed. This technique is fully compatible with the use of widening, and whenever it applies, it generally improves both the precision and the performances of the analysis.

Data and Resources

Additional Info

Field Value
Source https://hal.science/hal-00785116
Author Gonnord, Laure, Halbwachs, Nicolas
Maintainer CCSD
Last Updated May 14, 2026, 16:32 (UTC)
Created May 14, 2026, 16:32 (UTC)
Identifier hal-00785116
Language en
Rights https://about.hal.science/hal-authorisation-v1/
contributor Laboratoire d'Informatique Fondamentale de Lille (LIFL) ; Université de Lille, Sciences et Technologies-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lille, Sciences Humaines et Sociales-Centre National de la Recherche Scientifique (CNRS)
creator Gonnord, Laure
date 2010-03-03T00:00:00
harvest_object_id e0d59278-3af9-41df-a5d6-cd02e6f9fd8f
harvest_source_id 3374d638-d20b-4672-ba96-a23232d55657
harvest_source_title test moissonnage SELUNE
metadata_modified 2025-09-27T00:00:00
set_spec type:REPORT