Cours

CS-550: Formal verification

Résumé

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 the practice behind them.

Séances de cours

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

Page Moodle

http://go.epfl.ch/CS-550

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.

Résumé

Séances de cours

Enseignant·e

Viktor Kuncak

Source officielle

Page Moodle

http://go.epfl.ch/CS-550

Séances de ce cours (58)

Vérification formelle et synthèse des programmes

Par l’instructeur Viktor Kuncak explore les activités de vérification formelle, de synthèse de programme et d’enseignement à l’EPFL.

Qu’est-ce que la vérification formelle?

Introduit la vérification formelle et ses avantages par rapport aux méthodes de test traditionnelles, en discutant de la démonstration automatique des théorèmes et en compilant les déclarations d'exactitude dans des conditions de vérification.

Premiers pas avec Stainless

Introduit Stainless, un vérificateur pour Scala, mettant l'accent sur la prévention des bugs et l'accès à la bibliothèque.

Assertions auxiliaires en acier inoxydable

Présente l'utilisation d'assertions en Inox pour prouver les propriétés des fractions.

Déplier des fonctions récursives en Inox

Couvre le concept de déploiement des fonctions récursives à l'aide de l'outil Inoxydable.

Afficher plus

Cours associés (32)

ME-213: Programmation pour ingénieur

Mettre en pratique les bases de la programmation vues au semestre précédent. Développer un logiciel structuré. Méthode de debug d'un logiciel. Introduction à la programmation scientifique. Introduction à l'instrumentation virtuelle. ...

PHYS-467: Machine learning for physicists

Machine learning and data analysis are becoming increasingly central in sciences including physics. In this course, fundamental principles and methods of machine learning will be introduced and practised. ...

ENG-209: Data science pour ingénieurs avec Python

Ce cours propose une immersion progressive et complète dans le domaine de la Data Science à travers le langage Python. Il guide les étudiants depuis la manipulation de données brutes jusqu'à la modélisation et l'extraction de connaissances utiles à partir ...

MATH-410: Riemann surfaces

This course is an introduction to the theory of Riemann surfaces. Riemann surfaces naturally appear is mathematics in many different ways: as a result of analytic continuation, as quotients of complex domains under discontinuous group actions, as algebraic ...

MATH-101(g): Analyse I

Étudier les concepts fondamentaux d'analyse et le calcul différentiel et intégral des fonctions réelles d'une variable. ...

Afficher plus