
Overview SLEEK is a prover for separation logic with frame inferring capability. Users can specify two heap states in separation formulae, and check 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 SLEEK prover. This residual heap state will include the pure state of the antecedent. SLEEK can also support instantiation of existential variables when they are written in the consequent as unbound variables. This technique allows instantiations to be carried out based on the program state at each call site. As part of the implication check, SLEEK converts its proof obligation to pure formulae which can be shipped to theorem provers, such as Omega, CVC Lite, MONA and Isabelle. Terms Entailment Separation Logic Frame Rule Pure Formula SLEEK  binary compiled under Fedora Core release 4. Works with provers, such as Omega Calculator, Isabelle, MONA, CVC Lite
Tutorial
o cvcl  Cvc Lite o omega  Omega Calculator {default} o co  Try first Cvc Lite if fail then try Omega Calculator o isabelle  Isabelle o mona  Mona o om  Try first Omega Calculator if fail then try Mona o oi  Try first Omega Calculator if fail then try Isabelle o Input format description o Base types: int, bool o Data structures can be declared. For example: data node { int val ; node next } Describes a structure called node with an integer field, val and a recursive node field next. o Separation formulas are given in disjunctive normal form, Each disjunct can have two parts: o heap formula o pure arithmetic formula The basic heap node is described by a v::node_type<list_of_arguments> where v denotes a pointer to the node, while list_of_arguments are the contents of the heap node. It can be viewed as a pointto heap structure which is often specified as v>node_type<list_of_arguments> in separation logic notation. 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 SLEEK is as follows: pred 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 it is made up of a node linked to a smaller list segment of length n1. Each predicate shall also have a formula to describe its pure invariant. For the lseg predicate, it’s pure formulae (without heap) n>=0. If not specified, the pure invariant is just assumed to be true. A free or an anonymous variable within a separation formula is always assumed to be existentially quantified. o Lemmas relating between heap predicate may also be defined. There are three classes of lemmas of simple form. This simple lemma form only has a single predicate in its LHS: lemma simple_LHS > formula_RHS lemma simple_LHS < formula_RHS lemma simple_LHS <> formula_RHS A more complex form of lemma allows multiple predicates on the LHS, together with universally quantified variables of form: clemma fomula_LHS > formula_RHS SLEEK can help prove each lemma and apply these lemmas automatically during entailment proving.
o Meta variables may also be declared. Some examples are: let $f1 = x::sortl<a, b> let $f2 = x::sortl<d, c> The variables $f1,$f2 can then be used instead of the formulas. For example: checkentail $f1  $f2 will actually check that x::sortl<a, b> entails x::sortl<d, c> The formulas can be also composed: let $v1 = x' = 1 let $v2 = x' = x + 1 let $v3 = compose[x]($v1; $v2) $v3 will represent the formula obtained by replacing all free occurrences of x in $v2 with $v1 Meta formula: A meta formula is either a meta variable, a normal formula or a composition. o Commands o checkentail meta_construct_1  meta_construct_2 Will try to check if meta_construct_1 implies meta_construct_2. It outputs valid, if so; and unknown otherwise. The residue of the last entailment will be stored in a variable called residue. o capture_residue meta_variable Will store the residue of the last entailment in the supplied metavariable. o print meta_variable Will print the formula stored in the metavariable. o print residue Will print the last residue formula.
Papers Enhancing Program Verification with Lemmas Huu Hai Nguyen and WeiNgan Chin CAV 2008 : 20th International Conference on Computer Aided Verification People Contributors to Sleek are: Huu Hai Nguyen 
