Stainless documentation

Contents:

• Introduction
  • Stainless and Scala
  • Software Verification
  • Program Termination
• Getting Started
• Installing Stainless
  • sbt
  • Linux & Mac OS-X
  • Windows
  • External Solvers
  • Running Tests
  • Building Stainless Documentation
  • Using Stainless in Eclipse
• Tutorial: Sorting
  • Warm-up: Max
  • Defining Lists and Their Properties
  • Insertion into Sorted List
  • Being Sorted is Not Enough
  • Using Size in Specification
  • Using Content in Specification
• Pure Scala
  • Boolean
  • TupleX
  • Int
  • BigInt
  • Real
  • Set
  • Functional Array
  • Map
  • Function
• Stainless Library
  • Annotations
  • List[T]
  • Set[T], Map[T]
• Imperative
  • Imperative Code
  • While loops
  • Arrays
  • Mutable Objects
  • Aliasing
  • Annotations for Imperative Programming
• Verification
  • Verification conditions
• Proving Theorems
  • A practical introduction to proofs
  • Techniques for proving non-trivial propositions
  • Techniques for proving non-trivial postconditions
  • A complex example: additivity of measures
  • Quick Recap
• Limitations of Verification
  • Out of Memory Errors
• Command Line Options
  • Choosing which Stainless feature to use
  • Additional top-level options
  • Additional Options (by component)
• Stainless Smart Contracts
  • Overview
  • Installation
  • Formal Verification of Smart Contracts
  • Compilation to Solidity
  • Features
  • Development
  • Known Issues
  • Reporting Issues
• Frequently Asked Questions
  • Proving properties of size
  • Compiling Stainless programs to bytecode
• References
  • Videos
  • Papers
  • Books
• Stainless’ Internals

• Search Page