University of Sussex
Browse

File(s) under permanent embargo

Abstract acceleration in linear relation analysis

journal contribution
posted on 2023-06-09, 00:30 authored by Laure Gonnord, Peter Schrammel
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 article 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.

History

Publication status

  • Published

File Version

  • Published version

Journal

Science of Computer Programming

ISSN

0167-6423

Publisher

Elsevier

Volume

93B

Page range

125-153

Department affiliated with

  • Informatics Publications

Full text available

  • No

Peer reviewed?

  • Yes

Legacy Posted Date

2016-05-09

First Compliant Deposit (FCD) Date

2016-05-09

Usage metrics

    University of Sussex (Publications)

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC