Interprocedural Context-Unbounded Program Analysis Using Observation Sequences
Abstract
A classical result by Ramalingam about synchronization-sensitive interprocedural program analysis implies that reachability for concurrent threads running recursive procedures is undecidable. A technique proposed by Qadeer and Rehof, to bound the number of context switches allowed between the threads, leads to an incomplete solution that is, however, believed to catch “most bugs” in practice, as errors tend to occur within few contexts. The question of whether the technique can also prove the absence of bugs at least in some cases has remained largely open.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Dec 07, 2020
- Source ID
- 10.1145/3418583
Entities
People
- Peizun Liu
- Thomas Reps
- Thomas Wahl
Organizations
- National Science Foundation
- Northeastern University
- Office of Naval Research
- University of Wisconsin–Madison