Here lie some fascinating example programs and their verifications.

======================
BONA FIDE CASE STUDIES
======================

SinglyLinkedList: is-null, length, rev, and append
Malloc: a naive memory allocator, used by the rest of the case studies
Sets: the finite set ADT, implemented by:
  ListSet: ...using unsorted lists
  TreeSet: ...using binary search trees
Bags: the bag ADT, implemented by:
  Queue: ...using a linked list to provide a FIFO interface
Memoize: an ADT that optimizes use of a stateful function (passed as a parameter at runtime) by caching results

================
REGRESSION TESTS
================

LemmaTests: proving some simple implications between separation logic assertions
Baby: some very basic programs that don't use separation logic explicitly
TrivialMem: a tiny step toward using separation logic and memory operations
TrivialMem2: another tiny step
Indir: let's access a pointer through a pointer!
Factorial: speaks for itself
Swap: let's swap the values in two memory addresses!
TrivialArray: array read and write functions, plus incrementing every cell of an array
Pair: a very basic stateful ADT: pairs of words, with read and write methods
