HIPimm: Verifying Granular Immutability Guarantees
HIPimm: Verifying Granular Immutability Guarantees
MENU




(online) EXAMPLEs


HIPimm's Overview

HIPimm, an extension of the HIP/SLEEK automatic verification system, offers immutability guarantees on top of ensuring functional correctness for heap-manipulating programs. The extra capability of HIPimm, as compared to its precursor, is the ability to reason about immutability guarantees in a granular manner. For this purpose, we enhance the specification language with immutability annotations which provide the means to assert whether the annotated heap parts of a data structure can be mutated or whether is inaccessible. As part of user defined predicates, these annotations are integrated at the data field level offering granular immutability guarantees. An immediate result of this new functionality is a finer level of precision in the verification process of programs involving heap data structures. That is, we enable the verification of program properties such as preservation of data structures shapes and/or values, flexible aliases, and information leakage prevention.

Downloads

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

Technical Report

Example programs

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




Please contact Andreea Costea if you have any problems/suggestions/discussions or simply want to learn more about HIPimm.