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

Déplier des fonctions récursives en Inox

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 couvre le concept de déploiement des fonctions récursives à l'aide de l'outil Stainless, en se concentrant sur des exemples tels que les fonctions de puissance et de plus, ainsi que leurs propriétés et postconditions.

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

Postcondition

In computer programming, a postcondition is a condition or predicate that must always be true just after the execution of some section of code or after an operation in a formal specification. Postconditions are sometimes tested using assertions within the code itself. Often, postconditions are simply included in the documentation of the affected section of code. For example: The result of a factorial is always an integer and greater than or equal to 1.

Programmation par contrat

La programmation par contrat (en anglais, design by contract ou DBC) est un paradigme de programmation dans lequel le déroulement des traitements est régi par des règles. Ces règles, appelées des assertions, forment un contrat qui précise les responsabilités entre le client et le fournisseur d'un morceau de code logiciel. C'est une méthode de programmation semi-formelle dont le but principal est de réduire le nombre de bugs dans les programmes.

Principe de substitution de Liskov

vignette|Barbara Liskov en 2010 Le principe de substitution de Liskov (LSP) est, en programmation orientée objet, une définition particulière de la notion de sous-type. Il a été formulé par Barbara Liskov et Jeannette Wing dans un article intitulé Family Values: A Behavioral Notion of Subtyping : Liskov et Wing en ont proposé la formulation condensée suivante : Si est une propriété démontrable pour tout objet de type , alors est vraie pour tout objet de type tel que est un sous-type de .

Logique de Hoare

La logique de Hoare, parfois appelée logique de Floyd-Hoare, est une méthode formelle définie par le chercheur en informatique britannique Tony Hoare dans un article de 1969 intitulé An Axiomatic Basis for Computer Programming. La méthode de Hoare met en place un formalisme logique permettant de raisonner sur la correction des programmes informatiques. Elle est fondée sur la syntaxe en ce sens que la correction d'un programme est décrite et démontrée par induction (récurrence) sur la structure du programme : à chaque règle syntaxique de construction d'un programme correspond une règle de la logique de Hoare.

Raffinement

En informatique, le raffinement consiste à détailler la conception pour arriver par itérations à l'implémentation finale. À chaque itération correspond un niveau de granularité de plus en plus fin. Quand cette technique est appliquée au code source, la conception est alors matérialisée par du pseudo-code. Cette technique peut aussi être appliquée au modèle de données.

Afficher plus

Séances de cours associées (15)

Programmes de vérification avec l'inox: Partie 2

Se concentre sur l'utilisation d'Inox pour la vérification des programmes, en démontrant le processus de vérification des programmes et en assurant l'exactitude.

Introduction à l'acier inoxydable: Premiers pas avec l'acier inoxydable

Introduit l'outil de vérification Stainless avec des exemples de vérification des propriétés de commutativité et des opérations arithmétiques.

Tutoriel en acier inoxydable: Demo.scala Basics

Couvre les bases de l'écriture et de la vérification du code Scala à l'aide du fichier Demo.scala.

Hoare Logic : Postconditions et Préconditions

Couvre la logique Hoare, les postconditions, les conditions préalables et les preuves de comportement du programme.

Compilateur de vérification: Approche Spec#

Explore le système de programmation Spec#, en se concentrant sur un compilateur de vérification pour C# 2.0.

Afficher plus

Concepts associés (23)

Postcondition

Programmation par contrat

Principe de substitution de Liskov

Logique de Hoare

Raffinement

Afficher plus