Stainless documentation¶
Contents:
- Introduction
- Installing Stainless
- Verifying and Compiling Examples
- Tutorial: Sorting
- Specifying Options
- Verification conditions
- Specifying Algebraic Properties
- Imperative
- Equivalence Checking
- Ghost Context
- Working With Existing Code
- Pure Scala
- Stainless Library
- Generating C Code
- Proving Theorems
- Limitations of Verification
- Case Studies
- Translation from Stainless to Coq
- Frequently Asked Questions
- References
- Stainless’ Internals