[ThreadHIP] Threads as Resource for Concurrency Verification

By Duy-Khanh Le, Wei-Ngan Chin and Yong-Meng Teo

ThreadHIP's Overview

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:

Downloads

Latest ThreadHIP's bundle (~80MB) - self-contained withThreadHIP, ParaHIP, and all experimental programs.

Technical Report

Example programs

Example programs (on the left panel) can be run ONLINE. More programs can be found in our Download page