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

Séance de cours

Tutoriel en acier inoxydable

Dans cours

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

Cette séance de cours présente un tutoriel sur la façon d'installer et d'utiliser Stainless, un outil de vérification des programmes Scala. L'instructeur démontre le processus d'installation, y compris le téléchargement de la dernière version à partir de GitHub, le dézippage du contenu et la liaison de l'exécutable à un dossier dans le chemin. Le tutoriel se termine par une étape de vérification pour assurer la bonne installation.

Enseignant·e

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.

Source officielle

Concepts associés (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.

Installation vidéo

vignette|Example d'installation vidéo Linstallation vidéo est une forme d'art contemporain qui combine la technologie vidéo avec l'art de l'installation, utilisant tous les aspects de l'environnement pour affecter le public. Faisant remonter ses origines à la naissance de l'art vidéo dans les années 1970, l'installation vidéo gagne en popularité à mesure que la technologie de production vidéo numérique devient plus facilement accessible.