

HIP/SLEEK Overview
The HIP/SLEEK systems are aimed at automatic verification
of functional correctness of heap manipulating programs.
HIP is a separation logic based automated verification system
for a simple imperative language, able to modularly verify
the specifications of heapmanipulating programs. The
specification language allows user defined inductive predicates
used to model complex data structures. Specifications
can contain both heap constraints and various pure constraints
like arithmetic constraints, bag constraints. Based on
given annotations for each method/loop, HIP will construct
a set of separation logic proof obligations in the form of formula
implications which are sent to the SLEEK separation
logic prover. SLEEK is a fully automatic prover for separation
logic with frame inferring capability.
Downloads
HIP/SLEEK Virtual Appliance
CS3234 HIP/SLEEK bundle the version used during the CS3234 lecture on HIP/SLEEK
HIPTnT bundle self contained bundle for hip with termination logic
HIP bundle self contained for hip with solutions to VSTTE 2012 competition
Older HIP executable
SLEEK executable
SLEEK bundle self contained for sleek to SMT 2014 competition
SCALA frontend for SLEEK
Work with provers, such as
Omega Calculator,
Isabelle,
MONA,
CVC Lite,
Z3
Terms of Usage
HIP 1.0 software release is freely available for academic and noncommercial use. The tar file distributed contains hip executable and a brief manual for its usage. The bundle also contains for your convenience executables for third party provers, e.g. Omega calculator for which their original usage/licencing requirements apply.
Description
HIP is a separation logic based automated verification system for a simple imperative language, able to modularly verify
heapmanipulating programs. The system can handle programs with complex data structures. It accepts abstract descriptions for such structures
in the form of inductive predicates. Predicates are represented as separation logic formulae that describe the shape of data structures together
with their derived properties, such as length, height and bag of values.
Given annotations for each method/loop with one or more pre/post conditions, the HIP verifier constructs a
set of obligations in the form of implication checks between pairs of formulae which are then sent to the SLEEK
prover to be discharged. The specification language allows rich specifications that contain both heap constraints expressed
as separation logic formulae and several different logic fragments like Presburger arithmetic, bags, lists for the
pure constraints. By making use of set/bag solvers, the user can also encode reachability conditions as a set/bag of
values that can be collected from some given data structure. Such conditions are then automatically discharged by HIP.
HIP relies on the SLEEK prover in order to discharge the verification conditions. SLEEK is a fully automatic
prover for separation logic with frame inferring capability. It takes as input two heap states represented by separation
formulae, and checks if one formula (the antecedent) entails the other (the consequent). The antecedent may cover
more heap states than the consequent, so a residual heap state which represents the frame condition can be returned by the
prover. This residual heap state will include the pure state of the antecedent. SLEEK also supports instantiation of logical
variables that appear during the entailment as existential variables in the consequent. As part of the implication check,
SLEEK discharges the heap obligations, the obligations pertaining to the shape of data structures and translates the remaining
pure obligations to pure constraints that can be discharged by theorem provers. The list of possible pure provers
includes Omega , MONA , CVC Lite, Z3, and Isabelle.
Usage
 Installation: unpack the archive and run ./make install
 Starting :
 ./hip [options] <source_file>
 ./sleek [options] <source_file>
 The underlying pure provers can be chosen with the tp option :
 cvcl  Cvc Lite
 oc  Omega Calculator {default}
 co  Try first Cvc Lite if fail then try Omega Calculator
 isabelle  Isabelle
 mona  Mona
 om  Try first Omega Calculator if fail then try Mona
 oi  Try first Omega Calculator if fail then try Isabelle
 set  Use Mona in set mode
 cm  CVC Lite then Mona
 z3  Z3
 HIP input format
The input file will be made up of three main parts:
 data declarations
 predicate definitions (including userspecified lemmas)
The predicate definition syntax :
pred_name <v^{*} > == Φ inv π ;
The predicate body Φ is a separation logic formula that provides information about the variables in the argument list. The predicate invariant π is a heap independent(pure) formula.
 The syntax for separation logic formulae is given below. By (x)^{*} we denote x zero or more times, (x)^{+} at least once, (x)^{?} at most once.
Φ := ψ  φ
ψ := χ  [ (χ or)^{+} ]
χ := case {(π > Ψ ;)^{+}}  [v^{*}] φ (ψ)^{?}
φ := φ or φ  (φ)  ω
 exists (v,)^{+}: ω
ω := (κ)^{?} & π ξ
ξ := (& FLOW= flow_name)^{?}
κ := True  κ * κ  v::struc_name < v^{*} > (@I)^{?}  v::pred_name < v^{*} > (@I)^{?}
π := True  False  exists (v^{+}:π) forall(v^{+}:π) π & π  (π  π)  ε < ε ε <= ε  ε > ε  ε >= ε 
ε = ε  ε != ε  ε in ε  ε notin ε  ε subset ε  bagmax(ε, ε)  bagmin (ε, ε)
ε inlist ε  ε notinlist ε  alln (ε , ε)  perm (ε , ε)
ε := id  null  int_const  float_const  (ε)  ε  ε+ε εε ε*ε
ε/ε  max(ε, ε)  min(ε, ε) 
{ε^{*}} union(ε^{*}) intersect(ε^{*}) diff(ε,ε)
[ε^{*}] ε:::ε tail(ε)  head(ε)  app(ε)  len(ε)  rev(ε)
 A formula can be given either in a disjunctive normal form (φ) or in a richer syntax with staging and case constructs (ψ).
In either case, the basic disjunct (ω) describes the heap shape (κ) pure constraints on the memory content (π) and
possibly flow information. The basic heap node is described by a v::node_type<list_of_arguments> where v denotes a pointer to
the node. If the node is an instance of a data structure, the arguments will refer to the structure fields else if the node is a predicate
instance, the arguments will capture the predicate arguments. Immutability can be enforced for each heap node by the use of the @I annotations.
 This format can be used to declare predicates for a wide range data structures. An example of a
predicate is lseg which describes a list segment of specified length. Its formal definition in HIP is as follows:
lseg<n, p> == self=p & n=0 or self::node<_,r> * r::lseg<n1,p> inv n>=0
It states that either the list segment is empty with length n=0, or or it is made up of a node linked to a
smaller list segment of length n1. Predicate invariants can be specified, for the lseg predicate, it's pure formulae (without heap) n>=0.
If not specified, the pure invariant is just assumed to be true.
 Lemmas relating heap predicates can also be defined. There are three classes of lemmas of simple form. By simple form we mean a lemma that has
a single predicate instance in its LHS (φ_{L}).
The lemma definition syntax is :
 lemma φ_{L} > φ_{R}
 lemma φ_{L} < φ_{R}
 lemma φ_{L} <> φ_{R}
 method declarations (with multiple pre/post conditions)
 A HIP input example:
The example given bellow defines a node structure, a predicate describing a singly linked list,
predicate that describes a sorted linked list and an append function that adds list y to the end of list x.
The sortl predicate also captures the smallest and the largest elements in the list.
The append method specification captures the fact that if given two linked lists then the result is a linked list of size equal to the sum of the two
lists lengths. Also if the input lists are sorted and the smallest element in y is larger than the largest
in x, then the resulting list is sorted.
data node { int val; node next; }
ll<n> == self=null & n=0 or self::node<_,p> *
p::ll<n1> inv n>=0;
sortl<mi,mx> == self::node<mi,null> & mi=mx or
self::node<mi,p> * p::sortl<m,mx> & mi<=m inv mi<=mx
& self!=null;
node append(node x, node y)
requires x::ll<n>*y::ll<m> & n>0
ensures res::ll<n+m> & res=x;
requires x::sortl<s1,b1> * y::sortl<s2,b2> & b1<=s2
ensures res::sortl<s1,b2> ;
requires x::sortl<s1,b1> & y=null
ensures res::sortl<s1,b1>;
{
node t;
t=x.next;
if (t==null) x.next=y;
else x.next=append(t,y);
return x;
}
Papers
 Cristina David, WeiNgan Chin : Immutable Specifications for More Concise and Precise Verification . OOPSLA 2011. [pdf]
 Cristian Gherghina, Cristina David, Shengchao Qin and WeiNgan Chin : Structured Specifications for Better Verification of HeapManipulating Programs. FM 2011. [pdf]
 WeiNgan Chin, Cristian Gherghina, Razvan Voicu, Quang Loc Le, Florin Craciun, Shengchao Qin :
A Specialization Calculus for Pruning Disjunctive Predicates to Support Verification. CAV 2011. [pdf]
 WeiNgan Chin, Cristina David, Huu Hai Nguyen, and Shengchao Qin : Automated Verification of Shape, Size and Bag Properties via UserDefined Predicates in Separation Logic. Science of Computer Programming 2011.
 Cristian Gherghina, Cristina David : A Specification Logic for Exceptions and Beyond. ATVA 2010. [pdf]
 Cristina David, Cristian Gherghina, WeiNgan Chin : Translation and Optimization for a Core Calculus with Exceptions. PEPM 2009.
[pdf]
 Huu Hai Nguyen and WeiNgan Chin : Enhancing Program Verification with Lemmas. CAV 2008 [ps]
 Huu Hai Nguyen, Cristina David, Shengchao Qin, WeiNgan Chin : Automated Verification of Shape and Size Properties via Separation Logic. VMCAI 2007.
[ps]
People
Contributors to HIP are:
