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. © Springer-Verlag Berlin Heidelberg 2007.
CITATION STYLE
Bouajjani, A., Fratani, S., & Qadeer, S. (2007). Context-bounded analysis of multithreaded programs with dynamic linked structures. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4590 LNCS, pp. 207–220). Springer Verlag. https://doi.org/10.1007/978-3-540-73368-3_24
Mendeley helps you to discover research relevant for your work.