|
|
HIP is an automated verification system based on separation logic for a simple imperative language. It is able to modularly verify heap-manipulating programs. Prior to verification, users are expected to define predicates in separation formulae to describe the shape of data structures together with their derived properties, such as length, height and bag of values. Users must also annotate each method/loop with one or more pre/post conditions prior to automated verification. HIP verifier eventually translates proof obligations to pure formulae that can be discharged by theorem provers, such as Omega (a Presburger prover), MONA (based on monadic second-order logic), CVC Lite (an SMT solver) or Isabelle (a general purpose theorem prover that is supported by some automatic tactics). With the help of set/bag solvers, it can also encode reachability as a set/bag of values that can be collected from some given data structure. Separation Logic Pre/Post Conditions Pure Provers HIP - binary compiled under Fedora Core release 4. Works with provers, such as Omega Calculator, Isabelle, MONA, CVC Lite o runs with: ./hip [options] <source_file> o underlying pure 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 set - Use Mona in set mode o cm - CVC Lite then Mona
o Input format description: The input file will be made up of several parts: o data declaration o predicate definition in separation logic (including user-specified lemmas) o method declarations (with multiple pre/post conditions)
Base types: int, bool Data structures can be declared. For example: data node { int val ; node next } Desribes a structure called node with an integer field, val and a recursive node field next.
Assertion formulas format: Separation formulas is given in disjunctive normal form, Each disjunct can have two parts: - heap formula - 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 points-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 HIP 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 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.
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
o An example data node { int val; node next; }
ll<n> == self=null & n=0 or self::node<_,p> * p::ll<n-1> 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; }
Enhancing Program Verification with Lemmas Huu Hai Nguyen and Wei-Ngan Chin CAV 2008 : 20th International Conference on Computer Aided Verification
Automated Verification of Shape and Size Properties via Separation Logic Huu Hai Nguyen, Cristina David, Shengchao Qin, Wei-Ngan Chin VMCAI 2007 : Eighth International Conference on Verification, Model Checking and Abstract Interpretation Contributors to HIP are: Huu Hai Nguyen |
||
|
|
|
|