ThreadHIP is a verifier for shared-memory concurrent programs with first-class threads. It employs a novel "threads as resource" approach. This approach allows the ownership of a thread (and its resource) to be flexibly split, combined, and (partially) transferred across procedure and thread boundaries. The approach has several advantages:
Latest ThreadHIP's bundle (~80MB) - self-contained withThreadHIP, ParaHIP, and all experimental programs.
Example programs (on the left panel) can be run ONLINE. More programs can be found in our Download page