HipCAP: A Concurrency Verification System
with Higher-Order Concurrent Abstract Predicates

Wei-Ngan Chin and Ton Chanh Le and Shengchao Qin




HipCAP is a concurrency verification system, which employs the concept of concurrent abstract predicates (CAP) for precisely tracking resource exchanges among concurrent threads. The system aims to formally prove three correctness properties of concurrent programs:

  1. race-freedom,
  2. deadlock-freedom and
  3. resource-preservation.

Currently, we are focusing on a formal verification solution for the versatile CountDownLatch (CDL) where multiple threads are involved in data exchanges during concurrency synchronization. CountDownLatch example programs (on the left panel) can be run ONLINE.

Please contact Ton Chanh Le if you have any problems/suggestions/discussions or simply want to learn more about HipCAP.