HIPComp: Specifying Compatible Sharing in Data Structures

By Asankhaya Sharma, Aquinas Hobor and Wei-Ngan Chin

HIPComp's Overview

HIPComp is a verifier for programs using data structures with compatible sharing. The user provides the specification in form of pre and post conditions for each method and the verifier automatically checks if the program satisfies its specification. The specification language of HIPComp extends separation logic with operators that allow sharing between heaps. The following sharing operators are used: * separating conjunction (for disjoint objects and partial fields), &* overlaid conjunction (for overlaid data structures) and & classical conjunction (for aliased objects and fields).

Downloads

Latest HIPComp's virtual machine (all-in-one ~4.6GB) - with HIPComp and prerequisite software pre-installed

Technical Report

Coq Documentation

Coq Proofs

Example programs

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