Skip to the content.

Verifying Programs with Stainless

About the tutorial

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.

This tutorial will provide 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.

To get the basic flavor of Stainless, you can also consult the documentation including this basic tutorial or watch a keynote from Lambda Days. The tutorial will also cover examples not presented previously that illustrate some of the recent features.

Location and date

Location: Swiss Tech Convention Center near the campus of EPFL in Lausanne, Switzerland (M1 Metro stop EPFL)

Time: Tuesday, March 1st, afternoon

Setup

Installation for Scala 3 front end version of Stainless

Program Schedule

Time Topic
afternoon Basics of Stainless
  Verifying imperative code
  Proof control
  An Extended Verification Example
  Features, Tips, and Case Studies