Context-bounded analysis of multithreaded programs with dynamic linked structures

A. Bouajjani, S. Fratani, and S. Qadeer

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 {\em 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.

Proceedings of the 19th International Conference on Computer Aided Verification (CAV 2007).