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
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.
Document type :
Conference papers
Complete list of metadata
Contributor : Bertrand Jeannet Connect in order to contact the contributor
Submitted on : Friday, February 8, 2013 - 2:06:22 PM
Last modification on : Tuesday, August 2, 2022 - 4:25:01 AM



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⟩



Record views