Mediaspace scheduled maintenance: Aug 25, 2026 07:00 - 12:00 AM. During this time, videos will be temporarily unavailable. Check status updates.

Lecture

Stainless Tutorial

In course

CS-550: Formal verification

We introduce formal verification as an approach for developing highly reliable systems. Formal verification finds proofs that computer systems work under all relevant scenarios. We will learn how to use formal verification tools and explain the theory and ...

Description

This lecture presents a tutorial on how to install and use Stainless, a tool for verification of Scala programs. The instructor demonstrates the installation process, including downloading the latest version from GitHub, unzipping the content, and linking the executable to a folder in the path. The tutorial concludes with a verification step to ensure the correct installation.

Instructor

Viktor Kuncak

Viktor Kunčak joined EPFL in 2007, after receiving a PhD degree from MIT. Since then has been leading the Laboratory for Automated Reasoning and Analysis and supervised at least 12 completed PhD theses. His works on languages, algorithms and systems for verification and automated reasoning. He served as an initiator and one of the coordinators of a European network (COST action) in the area of automated reasoning, verification, and synthesis. In 2012 he received a 5-year single-investigator European Research Council (ERC) grant of 1.5M EUR. His invited talks include those at Lambda Days, Scala Days, NFM, LOPSTR, SYNT, ICALP, CSL, RV, VMCAI, and SMT. A paper on test generation he co-authored received an ACM SIGSOFT distinguished paper award at ICSE. A PLDI paper he co-authored was published in the Communications of the ACM as a Research Highlight article. His Google Scholar profile reports an over-approximate H-index of 38. He was an associate editor of ACM Transactions on Programming Languages and Systems (TOPLAS) and served as a co-chair of conferences on Computer-Aided Verification (CAV), Formal Methods in Computer Aided Design (FMCAD), Workshop on Synthesis (SYNT), and Verification, Model Checking, and Abstract Interpretation (VMCAI). At EPFL he teaches courses on functional and parallel programming, compilers, and verification. He has co-taught the MOOC "Parallel Programming" that was visited by over 100'000 learners and completed by thousands of students from all over the world.

Official source

Related concepts (2)

Installation art

Installation art is an artistic genre of three-dimensional works that are often site-specific and designed to transform the perception of a space. Generally, the term is applied to interior spaces, whereas exterior interventions are often called public art, land art or art intervention; however, the boundaries between these terms overlap. Installation art can be either temporary or permanent. Installation artworks have been constructed in exhibition spaces such as museums and galleries, as well as public and private spaces.

Video installation

Video installation is a contemporary art form that combines video technology with installation art, making use of all aspects of the surrounding environment to affect the audience. Tracing its origins to the birth of video art in the 1970s, it has increased in popularity as digital video production technology has become more readily accessible. Today, video installation is ubiquitous and visible in a range of environments—from galleries and museums to an expanded field that includes site-specific work in urban or industrial landscapes.