University of Sussex
Browse
jsc12.pdf (309.33 kB)

Applying abstract acceleration to (co-)reachability analysis of reactive programs

Download (309.33 kB)
journal contribution
posted on 2023-06-09, 01:05 authored by Peter Schrammel, Bertrand Jeannet
Acceleration methods are commonly used for computing precisely the effects of loops in the reachability analysis of counter machine models. Applying these methods on synchronous data-flow programs, e.g. Lustre programs, requires to deal with the non-deterministic transformations due to numerical input variables. In this article, we address this problem by extending the concept of abstract acceleration of Gonnord et al. to numerical input variables. Moreover, we describe the dual analysis for co-reachability. We compare our method with some alternative techniques based on abstract interpretation pointing out its advantages and limitations. At last, we give some experimental results.

History

Publication status

  • Published

File Version

  • Submitted version

Journal

Journal of Symbolic Computation

ISSN

0747-7171

Publisher

Science Direct

Issue

12

Volume

47

Page range

1512-1532

Department affiliated with

  • Informatics Publications

Full text available

  • Yes

Peer reviewed?

  • Yes

Legacy Posted Date

2016-05-09

Usage metrics

    University of Sussex (Publications)

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC