Abstract Acceleration in Linear relation analysis (extended version)
type: Dataset
description: Linear relation analysis is a classical abstract interpretation based on an over-approximation of reachable numerical states of a program by convex polyhedra. Since it works with a lattice of infinite height, it makes use of a widening operator to enforce the convergence of fixed point computations. Abstract acceleration is a method that computes the precise abstract effect of loops wherever possible and uses widening in the general case. Thus, it improves both the precision and the efficiency of the analysis. This research report gives a comprehensive tutorial on abstract acceleration: its origins in Presburger-based acceleration including new insights w.r.t. the linear accelerability of linear transformations, methods for simple and nested loops, recent extensions, tools and applications, and a detailed discussion of related methods and future perspectives. This is the long version of a paper under submission.
issued: 2026-05-14T13:32:14.695479
language: en
modified: 2026-05-14T13:32:14.695483
contact point: Organization
  fn: CCSD
keyword: abstract-acceleration
keyword: infoeu-reposemanticsreport
keyword: infoinfo-pfcomputer-science-csperformance-cspf
keyword: infoinfo-sccomputer-science-cssymbolic-computation-cssc
keyword: linear-relation-analysis
keyword: reports
keyword: static-analysis
landing page: https://hal.science/hal-00787212

Abstract Acceleration in Linear relation analysis (extended version)
type: Distribution
format: HTML
issued: 2026-05-14T13:32:14.712701
modified: 2026-05-14T13:32:14.679002
access URL: https://hal.science/hal-00787212

test_moissonnage_selune
type: Agent