Deadlock Detection in Linear Recursive Programs

Elena Giachino 1, 2 Cosimo Laneve 1, 2
1 FOCUS - Foundations of Component-based Ubiquitous Systems
CRISAM - Inria Sophia Antipolis - Méditerranée , DISI - Dipartimento di Informatica - Scienza e Ingegneria [Bologna]
Abstract : Deadlock detection in recursive programs that admit dy-namic resource creation is extremely complex and solutions either give imprecise answers or do not scale. We define an algorithm for detecting deadlocks of linear recursive pro-grams of a basic model. The theory that underpins the algorithm is a generalization of the theory of permutations of names to so-called muta-tions, which transform tuples by introducing duplicates and fresh names. Our algorithm realizes the back-end of deadlock analyzers for object-oriented programming languages, once the association programs/basic-model-programs has been defined as front-end.
Type de document :
Communication dans un congrès
Formal Methods for Executable Software Models - 14th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, 2014, Jun 2014, Bertinoro, Italy. pp.26 - 64, 2014, 〈10.1007/978-3-319-07317-0_2〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01091747
Contributeur : Laneve Cosimo <>
Soumis le : samedi 6 décembre 2014 - 09:11:45
Dernière modification le : jeudi 11 janvier 2018 - 16:39:39
Document(s) archivé(s) le : lundi 9 mars 2015 - 06:06:51

Fichier

sfm-main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Elena Giachino, Cosimo Laneve. Deadlock Detection in Linear Recursive Programs. Formal Methods for Executable Software Models - 14th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, 2014, Jun 2014, Bertinoro, Italy. pp.26 - 64, 2014, 〈10.1007/978-3-319-07317-0_2〉. 〈hal-01091747〉

Partager

Métriques

Consultations de la notice

60

Téléchargements de fichiers

95