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, Principled Software Development, 2018. [Download (PDF, 603 KB)]

Additional information is available for download here:

• Download Challenge statement (PDF, 217 KB) (see problem 5)
• Provided Java implementation:
      Download BinomialHeapNode.java (JAVA, 435 Bytes)
      Download BinomialHeap.java (JAVA, 3 KB)
• Download Viper solution (VPR, 29 KB)