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

Peter Schrammel 1, * Bertrand Jeannet 1, *
* Auteur correspondant
1 POP ART - Programming languages, Operating Systems, Parallelism, and Aspects for Real-Time
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
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.
Type de document :
Article dans une revue
Journal of Symbolic Computation, Elsevier, 2012, 47 (12), pp.1512-1532. 〈10.1016/j.jsc.2011.12.051〉
Liste complète des métadonnées

Littérature citée [39 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00753412
Contributeur : Peter Schrammel <>
Soumis le : lundi 19 novembre 2012 - 13:46:20
Dernière modification le : jeudi 11 octobre 2018 - 08:48:03
Document(s) archivé(s) le : jeudi 21 février 2013 - 11:21:01

Fichiers

paper.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Peter Schrammel, Bertrand Jeannet. Applying abstract acceleration to (co-)reachability analysis of reactive programs. Journal of Symbolic Computation, Elsevier, 2012, 47 (12), pp.1512-1532. 〈10.1016/j.jsc.2011.12.051〉. 〈hal-00753412〉

Partager

Métriques

Consultations de la notice

248

Téléchargements de fichiers

247