Schrammel, Peter and Jeannet, Bertrand (2012) Applying abstract acceleration to (co-)reachability analysis of reactive programs. Journal of Symbolic Computation, 47 (12). pp. 1512-1532. ISSN 0747-7171
![]() |
PDF
- Submitted Version
Download (316kB) |
Abstract
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.
Item Type: | Article |
---|---|
Keywords: | Static analysis; Acceleration; Abstract interpretation; Linear relation analysis |
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 11:10 |
Last Modified: | 18 Mar 2017 11:05 |
URI: | http://srodev.sussex.ac.uk/id/eprint/60806 |
View download statistics for this item
📧 Request an update