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 and arrays. The specification logic supports data types such as mathematical sets and maps as well as user-defined algebraic data types, predicates, and functions.

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:

• all procedures mutually satisfy their specified contracts,
• all loops satisfy their loop invariants,
• all heap accesses and memory deallocations are safe,
• 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.

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 download and installation instructions please visit the tool's GitHub repository.

Publications

1. Go with the Flow: Compositional Abstractions for Concurrent Data Structures pdf

   S. Krishna, D. Shasha, and T. Wies
   In Proceedings of ACM Symposium on the Principles of Programming Languages (POPL), 2018

2. Deciding Local Theory Extensions via E-Matching pdf

   K. Bansal, T. King, A. Reynolds, C. Barrett, and T. Wies
   In Proceedings of Computer Aided Verification (CAV), 2015

3. Automating Separation Logic with Trees and Data pdf

   R. Piskac, T. Wies, and D. Zufferey
   In Proceedings of Computer Aided Verification (CAV), 2014

4. GRASShopper: Complete Heap Verification with Mixed Specifications pdf

   R. Piskac, T. Wies, and D. Zufferey
   In Proceedings of Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2014

5. Automating Separation Logic using SMT pdf

   R. Piskac, T. Wies, and D. Zufferey
   In Proceedings of Computer Aided Verification (CAV), 2013