BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Stainless as a Verifying Compiler - Viktor Kuncak (EPFL - Ecole Po
 lytechnique Fédérale de Lausanne)
DTSTART:20220704T101500Z
DTEND:20220704T111500Z
UID:TALK175769@talks.cam.ac.uk
DESCRIPTION:Stainless ( https://github.com/epfl-lara/stainless/ ) is an op
 en-source system for constructing formally-verified software. Its developm
 ent spans a decade of work of members of the LARA group at EPFL. The prima
 ry input to Stainless is a subset of Scala\, whose detailed correctness pr
 operties can be proven or disproven. The same input can then run using sta
 ndard Scala compilers. In addition\, Stainless can translate programs with
  pre-allocated memory to C\, which can be processed using conventional C c
 ompilers\, eliminating the gap between verified models and implementations
  running on embedded devices.\nI will outline main design decisions behind
  Stainless\, including the use of a unified specification and implementati
 on language\, SMT solvers for automation\, as well as fair unrolling of re
 cursive functions and their specifications as a unifying proof automation 
 approach. This simple design allows finding counterexamples but also speci
 fying the desired inductive proofs of theorems. I will outline case studie
 s we used to evaluate the practicality of building verified software. Time
  permitting\, I will mention our experience in proving function equivalenc
 e for student assignments and a more recent project in which we are buildi
 ng a foundational proof assistant aimed at proving properties where detail
 ed user insights is necessary.
LOCATION:Seminar Room 1\, Newton Institute
END:VEVENT
END:VCALENDAR