University of Sussex
Browse

File(s) not publicly available

Abstract acceleration of general linear loops

Version 2 2023-06-12, 06:37
Version 1 2023-06-09, 00:30
conference contribution
posted on 2023-06-12, 06:37 authored by Bertrand Jeannet, Peter Schrammel, Sriram Sankaranarayanan
We present abstract acceleration techniques for computing loop invariants for numerical programs with linear assignments and conditionals. Whereas abstract interpretation techniques typically over-approximate the set of reachable states iteratively, abstract acceleration captures the effect of the loop with a single, non-iterative transfer function applied to the initial states at the loop head. In contrast to previous acceleration techniques, our approach applies to any linear loop without restrictions. Its novelty lies in the use of the Jordan normal form decomposition of the loop body to derive symbolic expressions for the entries of the matrix modeling the effect of ? = ? iterations of the loop. The entries of such a matrix depend on ? through complex polynomial, exponential and trigonometric functions. Therefore, we introduces an abstract domain for matrices that captures the linear inequality relations between these complex expressions. This results in an abstract matrix for describing the fixpoint semantics of the loop. Our approach integrates smoothly into standard abstract interpreters and can handle programs with nested loops and loops containing conditional branches. We evaluate it over small but complex loops that are commonly found in control software, comparing it with other tools for computing linear loop invariants. The loops in our benchmarks typically exhibit polynomial, exponential and oscillatory behaviors that present challenges to existing approaches. Our approach finds non-trivial invariants to prove useful bounds on the values of variables for such loops, clearly outperforming the existing approaches in terms of precision while exhibiting good performance.

History

Publication status

  • Published

File Version

  • Published version

Journal

POPL '14

Publisher

ACM

Volume

49

Page range

529-540

Pages

683

Event name

Principles of Programming Languages, POPL 2014

Event location

San Diego, California, USA

Event type

conference

Event date

January 2014

Book title

Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

Place of publication

New York, NY, United States

ISBN

9781450325448

Series

Principles of Programming Languages

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