Context-bounded analysis of multithreaded programs with dynamic linked structures

被引：0

作者：

Bouajjani, Ahmed ^{[1
]}

Fratani, Severine ^{[1
]}

Qadeer, Shaz ^{[2
]}

机构：

[1] CNRS, LIAFA, F-75700 Paris, France

[2] Microsoft Res, Redmond, WA USA

来源：

COMPUTER AIDED VERIFICATION, PROCEEDINGS | 2007年 / 4590卷

关键词：

D O I：

暂无

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

Bounded context switch reachability analysis is a useful and efficient approach for detecting bugs in multithreaded programs. In this paper, we address the application of this approach to the analysis of multithreaded programs with procedure calls and dynamic linked structures. We define a program semantics based on concurrent pushdown systems with visible heaps as stack symbols. A visible heap is the part of the heap reachable from global and local variables. We use pushdown analysis techniques to define an algorithm that explores the entire configuration space reachable under given bounds on the number of context switches and the size of visible heaps.

引用

页码：207 / +

页数：3