Viktor Kunčak is an associate professor in the School of Computer and Communication sciences of EPFL (Ecole Polytechnique Federale de Lausanne). He joined EPFL in 2007, after receiving a PhD degree from MIT. Since then has been leading the EPFL Laboratory for Automated Reasoning and Analysis (https://lara.epfl.ch). His research goal is to increase software reliability through new algorithms and tools for verification, synthesis, and automated reasoning.
I will give an overview of Stainless (https://stainless.epfl.ch).
Developers can use stainless to state and formally verify properties of functional programs written in Scala. I present foundation of stainless and its termination checks through an untyped functional language on top of which we impose a new type system, System FR. As an example of use case, I present how to build and develop verified hierarchy of algebraic structures, where Stainless proves laws when structures are instantiated.