VerifyThis Competition 2021: KIV Solutions

This Website documents the KIV solutions of the VerifyThis Competition held at ETAPS 2021 in Luxembourg, Luxembourg (virtual event). All proofs for challenge 2 were done during the competition, the solutions for challenges 1 and 3 were completed after the event.

KIV-Projects always link to an overview which gives the dependency graph of specifications. Clicking on one specification gives its text, and links to a theorem base summary (which lists names of theorems) and a theorem base listing (which shows the full sequent for each theorem). From there individual theorems and the full details of each proof are accessible.


Challenge 1

The Project Overview gives an overview of the entire specification hierarchy of our solution for challenge 1.

COMING SOON

Challenge 2

We were able to solve all tasks of Challenge 2 during the competition because we could use our library for Separation Logic as seen in the Project Overview. Here the heap is defined as an algebraic data type over references r and objects o with operations for allocation (h ++ r), deallocation (h -- r), and reading or updating objects at certain locations (h[r] or h[r, o] resp.). The specification heap-sep defines the common Separation Logic operators like the separating conjunction or the separating implication as higher order predcicates over the heap. The library also provides a heap-based definition of binary trees using generic nodes with left and right pointers. We reused these nodes for our definition of doubly-linked lists. The predicate dll(r, x)(h) abstracts the content of a heap h to an algebraic list x starting from reference r. An auxiliary predicate dlls(r, r0, r1, x)(h) is used to describe list segments in the heap, the references r0 and r1 point to the nodes to the left and right of the segment. Thus, dlls(r, null, null, x) is equivalent to dlls(r, x).

Having abstractions of the heap content to algebraic lists and to algebraic trees allows to formulate the required properties using these algebraic data types. The specification linked-tree-list defines the predicates ordered≤(t) and balanced(t) that in combination ensure that the algebraic tree t is a balanced search tree. An additional function t.toList calculates a algebraic list for a tree t that contains the same elements as t and maintains the order of t.

The algorithm for the construction of the binary search tree is implemented in the specification DLL2BST with the procedure dll_to_bst#. The auxiliary procedures size# and dll_to_bst_rec# are implemented in this specification as well. Note that we used natural numbers instead of integers in the declarations since negative values are not relevant for the task.

First, we proved the correctness of the size# procedure with the lemma dll-size-correct which states that if we have a valid doubly-linked list in the heap representing an algebraic list x, the result in count is the length # x of the list. The proof is by induction over the length of the list and was straightforward, however it was necessary to generalize the lemma by allowing a list segment separated from an arbitrary heap predicate hP.

The main effort was to prove the contract for dll_to_bst_rec#. We have to ensure that, given a valid list segment x in the heap, the execution of dll_to_bst_rec# yields a heap that contains the list segment x without its first n elements (restn(n, x)) and a balanced tree t containing the first n elements of x (t.toList = firstn(n, x)). The contract can be proven by induction over n, which again requires generalization to a heap with an additional separated heap predicate hP. After applying the induction hypothesis for both recursive calls it remains mainly to show that both subtrees and the new root node form a combined tree, see goal.

  ...
  (right0 => mknode(left0, b, root0) * tr(left0, t) * tr(root0, t0) * ...)(h2)
  ...
  ⊦ ∃ t. (tr(right0, t) * ...)(h2) ...
This is done with a few interactions by choosing the algebraic tree mkbranch(t, b, t0) for t and applying some lemmas from the Separation Logic library. The balanced and same-elements properties for the combined tree are proven automatically using lemmas from linked-tree-list.

Finally, the main proof obligation dll_to_bst_correct can be proven by simply applying the contracts of the two auxiliary procedures:

  dll(head, x)(h), ordered≤(x)
  ⊦ ⦉dll_to_bst#(head; h; root)⦊
      ∃ t. tr(root, t)(h) ∧ t.toList = x ∧ ordered≤(t) ∧ balanced(t)
Note that we did not have to prove in dll_to_bst_rec_correct that the resulting tree is ordered≤. Instead, ordered≤(t) follows directly from ordered≤(x) and t.toList = x (see this lemma).

We also solved the additional task and implemented an iterative version of size#: size_iter#. The correctness proof dll-size-iter-correct could be performed analogously using induction over the length of the list and the correctness of the corresponding main procedure dll_to_bst_iter# is again proven by using the contracts dll-size-iter-correct and dll_to_bst_rec_correct, see dll_to_bst_iter_correct.

Challenge 3

COMING SOON

Used basic libraries:

Back to the overview of all KIV projects.
For general informations on KIV and a download site for the whole system refer to this page.


[Imprint] [Data Privacy Statement]