Applying abstract acceleration to (co-)reachability analysis of reactive programs - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Article Dans Une Revue Journal of Symbolic Computation Année : 2012

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

Résumé

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.
Fichier principal
Vignette du fichier
paper.pdf (320.19 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-00753412 , version 1 (19-11-2012)

Identifiants

Citer

Peter Schrammel, Bertrand Jeannet. Applying abstract acceleration to (co-)reachability analysis of reactive programs. Journal of Symbolic Computation, 2012, 47 (12), pp.1512-1532. ⟨10.1016/j.jsc.2011.12.051⟩. ⟨hal-00753412⟩
227 Consultations
210 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More