title: Where does the KeY verification tool shine?
body: <p>What are some <strong>code examples</strong> demonstrating <a href="https://www.key-project.org/" rel="noreferrer">KeY</a>’s strength?</p>
  
  <p><strong>Details</strong></p>
  
  <p>With so many Formal Method tools available, I was wondering where KeY is better than its competition, and how? Some readable code examples would be quite helpful for comparison and understanding.</p>
  
  <p><strong>Updates</strong></p>
  
  <p>Searching through <a href="https://www.key-project.org" rel="noreferrer">the KeY website</a>, I found code examples from <a href="https://www.key-project.org/thebook2/examples-from-the-book/" rel="noreferrer">the book</a> — is there a suitable code example in there somewhere?</p>
  
  <p>Furthermore, I found <a href="http://envisage-project.eu/wp-content/uploads/2015/02/sorting.pdf" rel="noreferrer">a paper about the bug that KeY found in Java 8’s mergeCollapse in TimSort</a>. What is a minimal code from TimSort that demonstrates KeY’s strength? I do not understand, however, why model checking supposedly cannot find the bug — a bit array with 64 elements should not be too large to handle. Are other deductive verification tools just as capable of finding the bug?</p>
  
  <p>Is there an established verification competition with suitable code examples? </p>