Stainless as a Verifying Compiler

Add to your list(s) Download to your calendar using vCal

• Viktor Kuncak (EPFL - Ecole Polytechnique Fédérale de Lausanne)
• Monday 04 July 2022, 11:15-12:15
• Seminar Room 1, Newton Institute.

If you have a question about this talk, please contact nobody.

VS2W01 - Vistas in Verified Software

Stainless ( https://github.com/epfl-lara/stainless/ ) is an open-source system for constructing formally-verified software. Its development spans a decade of work of members of the LARA group at EPFL . The primary input to Stainless is a subset of Scala, whose detailed correctness properties can be proven or disproven. The same input can then run using standard Scala compilers. In addition, Stainless can translate programs with pre-allocated memory to C, which can be processed using conventional C compilers, eliminating the gap between verified models and implementations running on embedded devices. I will outline main design decisions behind Stainless, including the use of a unified specification and implementation language, SMT solvers for automation, as well as fair unrolling of recursive functions and their specifications as a unifying proof automation approach. This simple design allows finding counterexamples but also specifying the desired inductive proofs of theorems. I will outline case studies we used to evaluate the practicality of building verified software. Time permitting, I will mention our experience in proving function equivalence for student assignments and a more recent project in which we are building a foundational proof assistant aimed at proving properties where detailed user insights is necessary.

This talk is part of the Isaac Newton Institute Seminar Series series.

This talk is included in these lists:

• All CMS events
• Featured lists
• INI info aggregator
• Isaac Newton Institute Seminar Series
• School of Physical Sciences
• Seminar Room 1, Newton Institute
• bld31

Note that ex-directory lists are not shown.