This directory contains CIVL's solution for the challenge 4 of
VerifyThis 2017 Competition.  Detailed description of challenge 4 can
be found in :
"https://www.ethz.ch/content/dam/ethz/special-interest/infk/chair-program-method/pm/documents/Verify%20This/challenge4.pdf"

There are three different versions of the treeBuffer
implementations. All of them share the same header "treeBuffer.h":
  1) the naive implementation

  2) the caterpillar implementation

  3) the real implementation (modified based on the code from github https://github.com/rgrig/treebuffers):


For verification task 1:
    We use CIVL to compare the naive and caterpillar versions with a bound 5 on the 
newly added nodes.  


For verification task 2:
  CIVL's solution for the verification task of proving the space
efficiency of the real-time tree buffer data structure.  We used the
verbose implementation that goes along with the "Tree Buffer" paper.
(Grigore R., Kiefer S. (2015) Tree Buffers. In: Kroening D., Păsăreanu
C. (eds) Computer Aided Verification. CAV 2015. Lecture Notes in
Computer Science, vol 9206. Springer, Cham)

  A driver "driver_heap_bound.cvl" performs an arbitrary sequence of
add operations.  After each operation, the actual heap size is
compared with the heap size bound claimed in the paper.  CIVL has a
full memory heap model and provides a system function for accessing
the actual heap size.  We proved that, the memory usage of a tree
buffer after a bounded number of arbitrary operations is less than or
equal to the claimed heap size bound.

