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

Vérification formelle et synthèse des programmes

Dans cours

CS-320: Computer language processing

We teach the fundamental aspects of analyzing and interpreting computer languages, including the techniques to build compilers. You will build a working compiler from an elegant functional language into machine code using a popular backend called LLVM (htt ...

Description

Cette séance de cours couvre le travail de recherche de l'instructeur, Viktor Kuncak, dans la vérification formelle et la synthèse de programmes, en se concentrant sur la déduction automatisée, la démonstration de théorèmes, les procédures de décision et les méthodes déclaratives pour simplifier les tâches de programmation. Viktor Kuncak est professeur associé à l’EPFL et dirige un groupe de recherche dédié à la démonstration automatique de l’exactitude des programmes. Il donne également des cours sur la programmation fonctionnelle, le parallélisme, les compilateurs et la vérification.

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

Démonstration automatique de théorèmes

La démonstration automatique de théorèmes (DAT) est l'activité d'un logiciel qui démontre une proposition qu'on lui soumet, sans l'aide de l'utilisateur. Les démonstrateurs automatiques de théorème ont résolu des conjectures intéressantes difficiles à établir, certaines ayant échappé aux mathématiciens pendant longtemps ; c'est le cas, par exemple, de la , démontrée en 1996 par le logiciel EQP.

Vérification formelle

In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics. Formal verification can be helpful in proving the correctness of systems such as: cryptographic protocols, combinational circuits, digital circuits with internal memory, and software expressed as source code.

Méthode formelle (informatique)

En informatique, les méthodes formelles sont des techniques permettant de raisonner rigoureusement, à l'aide de logique mathématique, sur un programme informatique ou du matériel électronique numérique, afin de démontrer leur validité par rapport à une certaine spécification. Elles reposent sur les sémantiques des programmes, c'est-à-dire sur des descriptions mathématiques formelles du sens d'un programme donné par son code source (ou, parfois, son code objet).

Démonstration (logique et mathématiques)

vignette| : un des plus vieux fragments des Éléments d'Euclide qui montre une démonstration mathématique. En mathématiques et en logique, une démonstration est un ensemble structuré d'étapes correctes de raisonnement. Dans une démonstration, chaque étape est soit un axiome (un fait acquis), soit l'application d'une règle qui permet d'affirmer qu'une proposition, la conclusion, est une conséquence logique d'une ou plusieurs autres propositions, les prémisses de la règle.

Compilateur

En informatique, un compilateur est un programme qui transforme un code source en un code objet. Généralement, le code source est écrit dans un langage de programmation (le langage source), il est de haut niveau d'abstraction, et facilement compréhensible par l'humain. Le code objet est généralement écrit en langage de plus bas niveau (appelé langage cible), par exemple un langage d'assemblage ou langage machine, afin de créer un programme exécutable par une machine.

Afficher plus

Séances de cours associées (31)

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.

Vérification des compilateurs : défis et avantages

Examine les défis et les avantages de la vérification des compilateurs, en soulignant l'importance de la vérification des compilateurs pour les logiciels critiques.

Exactitude des compilateurs: Partie 2

Explore l'exactitude des compilateurs, en mettant l'accent sur l'évaluation des expressions, la compilation bytecode et les opérations de pile.

Exactitude des compilateurs: Partie 1

Explore l'exactitude du compilateur, des exemples de compilateurs vérifiés, la vérification formelle et les défis des compilateurs de certification.

Coq: Vue d'ensemble

Présente Coq et se concentre sur la démonstration du théorème et du _comm étape par étape.

Afficher plus

Concepts associés (19)

Démonstration automatique de théorèmes

Vérification formelle

Méthode formelle (informatique)

Démonstration (logique et mathématiques)

Compilateur

Afficher plus