GRASShopper

About

GRASShopper is an experimental verification tool for programs that manipulate dynamically allocated data structures. GRASShopper programs can be annotated with specifications expressed in a decidable specification logic to check functional correctness properties. The logic supports mixing of separation logic and first-order logic assertions, yielding expressive yet concise specifications.

The input language of GRASShopper is a simple procedural imperative language that supports user-defined struct types. The specification logic supports user-defined predicates for specifying properties of data structures implemented with these struct types.

The following GRASShopper program declares a procedure concat that concatenates two singly-linked lists:


/* A node in a singly-linked list. */
struct Node {
  var next: Node;
}

/* Predicate denoting an acyclic singly-linked list 
 * starting from 'x'. */
predicate list(x: Node) {
  acc({ z: Node :: Btwn(next, x, z, null) && z != null }) &*& 
  Reach(next, x, null)
}

/* Concatenate two lists 'a' and 'b'. 
 * The result is a single list 'res'. */
procedure concat(a: Node, b: Node) 
  returns (res: Node)
  requires list(a) &*& list(b)
  ensures list(res)
{
  if (a == null) {
    return b;
  } else {
    var curr := a;

    while (curr.next != null) 
      invariant acc(curr) **- list(a)
    {
      curr := curr.next; 
    }
    curr.next := b;
    return a;
  }
}
      
Given an input program, GRASShopper checks that:

  1. all procedures mutually satisfy their specified contracts,
  2. all loops satisfy their loop invariants,
  3. all heap accesses and memory deallocations are safe,
  4. there are no memory leaks.

The tool provides an Emacs mode with syntax highlighting and on-the-fly checking of GRASShopper programs. Errors in the program or its specification are automatically highlighted. There is also rudimentary support for the visualization of counterexample traces.

Limitations. At the moment, the tool is limited to reasoning about flat data structures such as singly-linked lists, doubly-linked list, binary search trees, etc. Work on adding support for arrays and nested linked data structures is ongoing.

Theory

Unlike other verification tools based on separation logic, GRASShopper does not implement a dedicated theorem prover for separation logic. Neither does it rely on user-guided proof search. Instead, the tool reduces proof obligations in separation logic to a decidable fragment of first-order logic, which we refer to as the Logic of Graph Reachability with Stratified Sets (GRASS). Reasoning in this logic is automated using conventional Satisfiability Modulo Theories solvers. This approach enables a robust combination of separation logic with other decidable first-order theories that are important in program verification. For example, GRASShopper can verify properties about data stored in heap-allocated structures (such as sortedness properties) even though there is no dedicated inbuilt support for this in the tool.

Download

GRASShopper is implemented in OCaml and distributed under a BSD license. We have tested the tool on Linux, Mac OS, and Windows/Cygwin.

For installation and usage, please follow the instructions in the README file.

People

The following people have contributed to GRASShopper:

Publications

Acknowledgments

This material is based in part upon work supported by the National Science Foundation under grant CCS-1320583. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the National Science Foundation.