Loading...
Please wait, while we are loading the content...
Similar Documents
Runtime Model Checking of Multithreaded C / C + + Programs
| Content Provider | Semantic Scholar |
|---|---|
| Author | Yang, Yu Chen, Xiaofang Gopalakrishnan, Ganesh Kirby, Robert Michael |
| Abstract | We present inspect, a tool for model checking safety properties of multithreaded C/C++ programs where threads interact through shared variables and synchronization primitives. The given program is mechanically transformed into an instrumented version that yields control to a centralized scheduler around each such interaction. The scheduler first enables an arbitrary execution. It then explores alternative interleavings of the program. It avoids redundancy exploration through dynamic partial order reduction(DPOR) [1]. Our initial experience shows that inspect is effective in testing and debugging multithreaded C/C++ programs. We are not aware of DPOR having been implemented in such a setting. With inspect, we have been able to find many bugs in real applications. |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | http://www.cs.utah.edu/research/techreports/2007/pdf/UUCS-07-008.pdf |
| Alternate Webpage(s) | http://www.cs.utah.edu/docs/techreports/2007/abstracts/UUCS-07-008a.pdf |
| Alternate Webpage(s) | http://www.cs.utah.edu/formal_verification/publications/conferences/pdf/spin07.pdf |
| Alternate Webpage(s) | http://formalverification.cs.utah.edu/publications/conferences/pdf/spin07.pdf |
| Alternate Webpage(s) | http://www.cs.utah.edu/docs/techreports/2007/pdf/UUCS-07-008.pdf |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
