jsc12.pdf (309.33 kB)
Applying abstract acceleration to (co-)reachability analysis of reactive programs
journal contribution
posted on 2023-06-09, 01:05 authored by Peter Schrammel, Bertrand JeannetAcceleration 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 ComputationISSN
0747-7171Publisher
Science DirectExternal DOI
Issue
12Volume
47Page range
1512-1532Department affiliated with
- Informatics Publications
Full text available
- Yes
Peer reviewed?
- Yes
Legacy Posted Date
2016-05-09Usage metrics
Categories
No categories selectedLicence
Exports
RefWorks
BibTeX
Ref. manager
Endnote
DataCite
NLM
DC