Stainless Verification System Tutorial by Viktor Kuncak and Jad Hamza, FMCAD 2021

Stainless GitHub page:

Also of interest may be examples in the Bolts repository

Section II Scala source files

Name		Name	Last commit message	Last commit date
Latest commit History 7 Commits
.gitignore		.gitignore
AddDigits.scala		AddDigits.scala
AddDigits0.scala		AddDigits0.scala
AmortizedQueue.scala		AmortizedQueue.scala
BinarySearch1.scala		BinarySearch1.scala
Diffs.scala		Diffs.scala
Diffs0.scala		Diffs0.scala
DiffsExplained.scala		DiffsExplained.scala
EnqueueTemplate.scala		EnqueueTemplate.scala
FindIndex.scala		FindIndex.scala
FindIndexOptionIff.scala		FindIndexOptionIff.scala
IEEEtran.bst		IEEEtran.bst
Max1.scala		Max1.scala
Max2.scala		Max2.scala
MaxBug.scala		MaxBug.scala
MaxBugOut.txt		MaxBugOut.txt
Queue0.scala		Queue0.scala
Queue1.scala		Queue1.scala
README.md		README.md
SimpleQueue.scala		SimpleQueue.scala
Stainless-Tutorial-FMCAD2021.pdf		Stainless-Tutorial-FMCAD2021.pdf
Undiffs.scala		Undiffs.scala
design.tex		design.tex
digits.tex		digits.tex
fmcad.cls		fmcad.cls
functional.tex		functional.tex
imperative.tex		imperative.tex
intro.tex		intro.tex
lstsettings.tex		lstsettings.tex
main.bib		main.bib
main.tex		main.tex
proofs.tex		proofs.tex
property0.scala		property0.scala
property1.scala		property1.scala
queue.tex		queue.tex
r		r
slides.pdf		slides.pdf
start.tex		start.tex
tutorial-stainless-copyright_form.pdf		tutorial-stainless-copyright_form.pdf