Binomial Heap Challenge

This page contains details on the Viper solution to the Binomial Heap verification challenge from the VSComp 2014 verification competition. An overview of the solution is presented in the following paper:

P. Müller: Binomial Heaps: A Case Study in Permission-Based Verification, 2018. To appear. [Download (PDF, 603 KB)vertical_align_bottom]

Additional information is available for download here:

• DownloadChallenge statement (PDF, 217 KB)vertical_align_bottom (see problem 5)
• Provided Java implementation:
      DownloadBinomialHeapNode.java (JAVA, 435 Bytes)vertical_align_bottom
      DownloadBinomialHeap.java (JAVA, 3 KB)vertical_align_bottom
• DownloadViper solution (VPR, 29 KB)vertical_align_bottom