Skip to the content.

Verifying Programs with Stainless

Stainless is an open-source system for constructing formally-verified software that is guaranteed to meet specifications for all inputs. The primary input format to Stainless is a subset of Scala. In addition, programs designed to run with pre-allocated memory (e.g., on an embedded system) can be translated to C and processed using conventional C compilers.

About the tutorial

This tutorial provides a hands-on introduction to Stainless through a series of guided examples. We will assume only basic programming skills; no particular background in verification or Scala is required, though a basic understanding of functional programming concepts will be helpful.

Program Schedule

Click here for the slides

Time Topic  
9:00-9:45 Part 1: Introduction (Georg S. Schmid, video)  
9:45-11:00 Part 2: Using stainless (Viktor Kunčak, video)  
11:30-12:15 Part 3: How Stainless works (Nicolas Voirol, video)  
12:15-12:50 Part 4: An Extended Verification Example (Mario Bucev, video)  

More in-depth resources:

For high-level overview you can also watch a keynote from Lambda Days or check a different and shorter tutorial at FMCAD 2021 including a video.


Live tutorial for which this content was created

The tutorial was originally given as part of ASPLOS 2022 conference on Tuesday, March 1st, at 09:00am-13:00 Lausanne (and Paris and Zurich) time zone. It was available on zoom as well as physically in Swiss Tech Convention Center near the campus of EPFL in Lausanne, Switzerland (M1 Metro stop EPFL)