Formal verification of Scala programs with Stainless – Romain Ruetschi скачать в хорошем качестве

Formal verification of Scala programs with Stainless – Romain Ruetschi

Everyone knows that writing bug-free code is fundamentally difficult, and that bugs will sometimes sneak in even in the presence of unit- or property-based tests. One solution to this problem is formal software verification. Formal verification allows users to statically verify that software systems will never crash nor diverge, and will in addition satisfy given functional correctness properties. In this talk, I will present Stainless, a verification system for an expressive subset of Scala. I will start by explaining what formal verification is, what are some of the challenges people encounter when putting it into practice, and how it can be made more practical. Then I will give a high-level overview of Stainless, and finally present a few verified programs, such as a small actor system, a parallel map-reduce implementation, as well as a little surprise! I’ll also demonstrate the tooling we have developed around Stainless which lets users easily integrate Stainless in their SBT-based Scala projects. Material * Slides: https://github.com/romac/talks/blob/m... Event * Typelevel Summit Lausanne, June 2019: https://typelevel.org/event/2019-06-s... About Speaker * I earned a MSc degree in Computer Science from EPFL in February 2018, and I have since been working at the Laboratory for Automated Reasoning and Analysis (LARA) at EPFL, under the supervision of Prof. Viktor Kunčak. I discovered Scala directly from Prof. Martin Ordersky during my Bachelor at EPFL a few years ago, and have never stopped learning more of it, alongside other languages such as Haskell, Rust or Idris. I am mainly interested in pure functional programming, type systems and formal methods. Licensing * This recording is licensed under CC-BY 4.0 (https://creativecommons.org/licenses/....