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).
Latest HIPComp's virtual machine (all-in-one ~4.6GB) - with HIPComp and prerequisite software pre-installed
Example programs (on the left panel) can be run ONLINE. More example programs and benchmarks can be found in our Download page