Séance de cours

Tutoriel en acier inoxydable

Graph Chat

Chattez avec Graph Search

Posez n’importe quelle question sur les cours, conférences, exercices, recherches, actualités, etc. de l’EPFL ou essayez les exemples de questions ci-dessous.

AVERTISSEMENT : Le chatbot Graph n'est pas programmé pour fournir des réponses explicites ou catégoriques à vos questions. Il transforme plutôt vos questions en demandes API qui sont distribuées aux différents services informatiques officiellement administrés par l'EPFL. Son but est uniquement de collecter et de recommander des références pertinentes à des contenus que vous pouvez explorer pour vous aider à répondre à vos questions.

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 (6)

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.

rc (for "run commands") is the command line interpreter for Version 10 Unix and Plan 9 from Bell Labs operating systems. It resembles the Bourne shell, but its syntax is somewhat simpler. It was created by Tom Duff, who is better known for an unusual C programming language construct ("Duff's device"). A port of the original rc to Unix is part of Plan 9 from User Space. A rewrite of rc for Unix-like operating systems by Byron Rakitzis is also available but includes some incompatible changes.

Terminal (informatique)

vignette|Un terminal DEC VT100. En informatique, un terminal est une variété de périphérique réseau placé à l'extrémité d'un nœud. Le terminal est un point d’accès de communication entre l'homme et un ordinateur central ou un réseau d'ordinateurs. Dans un réseau décentralisé de type client-serveur il correspond aujourd'hui à l'association minimale d'un périphérique de saisie (clavier) ou de pointage (souris) et d'un moniteur reliés à l'unité centrale.

Interface en ligne de commande

vignette|300px|Capture d'écran d'un shell Bash sous Gentoo. Une interface en ligne de commande ou ILC (en anglais command line interface, couramment abrégé CLI) est une interface homme-machine dans laquelle la communication entre l'utilisateur et l'ordinateur s'effectue en mode texte : l'utilisateur tape une ligne de commande, c'est-à-dire du texte au clavier pour demander à l'ordinateur d'effectuer une opération ; l'ordinateur affiche du texte correspondant au résultat de l'exécution des commandes tapées ou à des questions qu'un logiciel pose à l'utilisateur.