Gonnord, Laure and Schrammel, Peter (2014) Abstract acceleration in linear relation analysis. Science of Computer Programming, 93B. pp. 125-153. ISSN 0167-6423
![]() |
PDF
- Published Version
Restricted to SRO admin only Download (406kB) |
Abstract
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.
Item Type: | Article |
---|---|
Keywords: | Program analysis; Abstract interpretation; Linear relation analysis; Polyhedra; Acceleration |
Schools and Departments: | School of Engineering and Informatics > Informatics |
Subjects: | Q Science > QA Mathematics > QA0075 Electronic computers. Computer science |
Depositing User: | Peter Schrammel |
Date Deposited: | 09 May 2016 10:01 |
Last Modified: | 08 Mar 2017 05:09 |
URI: | http://srodev.sussex.ac.uk/id/eprint/59922 |
View download statistics for this item
📧 Request an update