Skip to Main content Skip to Navigation
Conference papers

Relational interprocedural verification of concurrent programs

Bertrand Jeannet 1, *
* Corresponding author
1 POP ART - Programming languages, Operating Systems, Parallelism, and Aspects for Real-Time
LIG - Laboratoire d'Informatique de Grenoble, Inria Grenoble - Rhône-Alpes
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.
Document type :
Conference papers
Complete list of metadata

https://hal.inria.fr/hal-00786350
Contributor : Bertrand Jeannet <>
Submitted on : Friday, February 8, 2013 - 2:06:22 PM
Last modification on : Tuesday, February 9, 2021 - 3:24:16 PM

Identifiers

Collections

CNRS | INRIA | LIG | UGA

Citation

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

Share

Metrics

Record views

211