Below are some simple examples to get the idea of how Stainless works; please contact LARA to learn about our larger case studies.

Example Buggy Programs

• invalid/BadConcRope.scala
• invalid/AbstractRefinementMap.scala
• invalid/AssociativityProperties.scala
• invalid/BraunTree.scala
• invalid/Choose.scala
• invalid/FunctionCaching.scala
• invalid/InsertionSort.scala
• invalid/ListOperations.scala
• invalid/Lists.scala
• invalid/Mean.scala
• invalid/PropositionalLogic.scala
• invalid/RedBlackTree2.scala
• invalid/SpecWithExtern.scala

Example Verified Programs

• valid/ConcRope.scala
• valid/AbstractRefinementMap.scala
• valid/AddingPositiveNumbers.scala
• valid/AssociativeList.scala
• valid/AssociativityProperties.scala
• valid/BinarySearchTreeQuant.scala
• valid/ChooseWithWitness.scala
• valid/FlatMap.scala
• valid/FoldAssociative.scala
• valid/Formulas.scala
• valid/FunctionCaching.scala
• valid/GuessNumber.scala
• valid/Heaps.scala
• valid/InsertionSort.scala
• valid/ListOperations.scala
• valid/Mean.scala
• valid/MergeSort.scala
• valid/PropositionalLogic.scala
• valid/QuickSort.scala
• valid/RedBlackTree.scala
• valid/StableSorter.scala