University of Utah
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'; grz 'at'; ganesh 'at'

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

Last updated on 7/11/10