Relational interprocedural verification of concurrent programs

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 : We propose a general analysis method for recursive, concurrent programs that tracks effectively procedure calls and returns in a concurrent context, even in the presence of unbounded recursion and infinite-state variables like integers. This method generalizes the relational interprocedural analysis of sequential programs to the concurrent case. We implemented it for programs with scalar variables, and we experimented several classical synchronisation protocols in order to illustrate the precision of our technique, but also to analyze the approximations it performs.
Type de document :
Communication dans un congrès
Software Engineering and Formal Methods, SEFM'09, Nov 2009, Hanoi, Vietnam. IEEE, 2009, 〈10.1109/SEFM.2009.29〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00786350
Contributeur : Bertrand Jeannet <>
Soumis le : vendredi 8 février 2013 - 14:06:22
Dernière modification le : mercredi 11 avril 2018 - 01:55:52

Identifiants

Collections

Citation

Bertrand Jeannet. Relational interprocedural verification of concurrent programs. Software Engineering and Formal Methods, SEFM'09, Nov 2009, Hanoi, Vietnam. IEEE, 2009, 〈10.1109/SEFM.2009.29〉. 〈hal-00786350〉

Partager

Métriques

Consultations de la notice

98