Stainless
0.9
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
FAQ: (Frequently) Asked Questions
References
Stainless’ Internals
Stainless
Stainless’ Internals
View page source
Stainless’ Internals
¶
The main component of Stainless and the dataflow in its pipeline:
