University of Utah
Search
School of Computing
Home People Research Admissions Site Map  

This is the homepage of Inspect, a dynamic verifier of C PThread programs.

Inspect framework diagram

Please visit Dr. Yu Yang's dissertation on Inspect, which is located here.

Inspect allows programmers to formally verify their PThread programs automatically for concurrency errors such as data races, deadlocks and assertion violations.

Inspect includes the following features:

Inspect utilizes static analysis methods to gather program information and instrument code. After static analysis, the program is executed under an external scheduler, exploring all relevant interleavings.

The Inspect tool is available for download here (please note that the sleep-set fix mentioned in this link has yet to be incorporated): [.zip]. General usage instructions are included in this [.pdf]. A tutorial presentation for Inspect can be downloaded here, along with the code examples [.zip]

You may visit the Gauss group's homepage to learn about all our formal verification work


Contact information: yuyang 'at' cs.utah.edu; grz 'at' cs.utah.edu; ganesh 'at' cs.utah.edu

School of Computing * 50 S. Central Campus Dr. Rm. 3190 * Salt Lake City, UT 84112
Disclaimer

Last updated on 7/11/10