Overview     
Terms
Software
Tutorial
Papers
People

SLEEK


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


Software

SLEEK - binary compiled under Fedora Core release 4.

Works with provers, such as Omega Calculator, Isabelle, MONA, CVC Lite

 


Tutorial
  •   Execution:
    • Running modes:
      • Interactive mode.

                ./sleek -int

                Commands are introduced one at a time. Each command is delimited by the dot symbol.

       

      •  Batch mode. A file containing all the commands is supplied.

                ./sleek <source files>

      • Underlying theorem provers can be chosen with -tp:

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 point-to 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<n-1,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 n-1. 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 meta-variable.                             

o    print meta_variable

Will print the formula stored in the meta-variable. 

o    print residue

      Will print  the last residue formula.




Papers

     Enhancing Program Verification with Lemmas

         Huu Hai Nguyen and Wei-Ngan Chin

         CAV 2008 : 20th International Conference on Computer Aided Verification


People

Contributors to Sleek are:

Wei-Ngan Chin

Huu Hai Nguyen

Cristina David

Cristian Gherghina