Treating for-Loops as First-Class Citizens in Proofs

Technical Report: Using Loop Scopes with for-Loops

Verifying OpenJDK's Sort Method for Generic Collections

TimSort is the main sorting algorithm provided by the Java standard library and many other programming frameworks. Our original goal was functional verification of TimSort with mechanical proofs. However, during our verification attempt we discovered …