University of Sussex
Browse

File(s) under permanent embargo

Logico-numerical abstract acceleration and application to the verification of data-flow programs

chapter
posted on 2023-06-09, 01:08 authored by Peter Schrammel, Bertrand Jeannet
Acceleration methods are commonly used for speeding up the convergence of loops in reachability analysis of counter machine models. Applying these methods to synchronous data-flow programs with Boolean and numerical variables, e.g., Lustre programs, requires the enumeration of the Boolean states in order to obtain a control flow graph (CFG) with numerical variables only. Our goal is to apply acceleration techniques to data-flow programs without resorting to this exhaustive enumeration. To this end, we present (1) logico-numerical abstract acceleration methods for CFGs with Boolean and numerical variables and (2) partitioning techniques that make logical-numerical abstract acceleration effective. Experimental results show that incorporating these methods in a verification tool based on abstract interpretation provides not only significant advantage in terms of accuracy, but also a gain in performance in comparison to standard techniques.

History

Publication status

  • Published

File Version

  • Accepted version

ISSN

0302-9743

Publisher

Springer

Volume

6887

Page range

233-248

Book title

Static Analysis

Series

Lecture Notes in Computer Science

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