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

Assertions auxiliaires 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 démontre l'utilisation d'assertions en Stainless, un système de vérification, à travers des exemples avec des fractions. L'instructeur explique comment définir des fractions, effectuer des opérations sur eux, et prouver des propriétés comme la commutativité et l'associativité en utilisant des assertions pour aider le prover théorème.

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

Fraction (mathématiques)

thumb|Trois quarts de gâteau, un quart ayant été retiré. En mathématiques, une fraction est un moyen d'écrire un nombre rationnel sous la forme d'un quotient de deux entiers. La fraction a/b désigne le quotient de a par b (b≠0). Dans cette fraction, a est appelé le numérateur et b le dénominateur. Une fraction représente un partage, le dénominateur représente le nombre de parts égales faites dans une unité et son numérateur représente le nombre de parts prises dans l'unité Un nombre que l'on peut représenter par des fractions de nombres entiers est appelé nombre rationnel.

Anneau commutatif

Un anneau commutatif est un anneau dans lequel la loi de multiplication est commutative. L’étude des anneaux commutatifs s’appelle l’algèbre commutative. Un anneau commutatif est un anneau (unitaire) dans lequel la loi de multiplication est commutative. Dans la mesure où les anneaux commutatifs sont des anneaux particuliers, nombre de concepts de théorie générale des anneaux conservent toute leur pertinence et leur utilité en théorie des anneaux commutatifs : ainsi ceux de morphismes d'anneaux, d'idéaux et d'anneaux quotients, de sous-anneaux, d'éléments nilpotents.

Fraction unitaire

Une fraction unitaire est un nombre rationnel écrit sous la forme d'une fraction où le numérateur est 1 et le dénominateur est un entier naturel non nul. Une fraction unitaire est par conséquent l'inverse d'un entier positif, 1/n, comme : 1/1, 1/2, 1/3, 1/42 etc. Multiplier deux fractions unitaires quelconques donne pour résultat une autre fraction unitaire : Par contre, additionner, soustraire, ou diviser deux fractions unitaires produit un résultat qui n'est généralement pas une fraction unitaire : 1/2 + 1/5 = 7/10 1/3 + 1/6 = 1/2 1/2 - 1/5 = 3/10 1/3 - 1/6 = 1/6 Les fractions unitaires jouent un rôle important dans l'arithmétique modulaire, comme elles peuvent être utilisées pour réduire la division modulaire lors du calcul des PGCD.

Associativité

En mathématiques, et plus précisément en algèbre générale, une loi de composition interne ou loi interne sur un ensemble E est dite associative si pour tous x, y et z dans E : En notant , l'associativité se traduit par le diagramme commutatif suivant : Parmi les lois associatives, on peut citer les lois d'addition et de multiplication des nombres réels, des nombres complexes et des matrices carrées, l'addition des vecteurs, et l'intersection, la réunion d'ensembles.

Associativité des puissances

En algèbre, l'associativité des puissances est une forme affaiblie de l'associativité. Un magma est dit associatif des puissances si le sous-magma engendré par n'importe quel élément est associatif. Concrètement, cela signifie que si une opération est effectuée plusieurs fois sur un même élément , l'ordre dans lequel sont effectuées ces opérations n'a pas d'importance ; ainsi, par exemple, . Tout magma associatif est évidemment associatif des puissances.

Afficher plus

Séances de cours associées (37)

Propriétés de la multiplication rationnelle

Couvre les propriétés de la multiplication rationnelle à travers des fractions et des calculs simples, conduisant à la résolution des problèmes de division.

Ajout de fractions

Couvre l'addition de fractions et de propriétés de nombres rationnels, en mettant l'accent sur l'associativité et les fractions de somme avec le même dénominateur.

Cohomologie Real Projective Space

Couvre la cohomologie dans les espaces projectifs réels, en se concentrant sur les propriétés associatives et les structures algébriques.

Nombres naturels

Couvre le concept de nombres naturels, y compris des propriétés telles que la commutativité et l'associativité.

Nombres naturels : Propriétés et opérations

Explore les nombres naturels, leurs propriétés, leurs opérations et les applications pratiques comme le calcul des heures en un an.

Afficher plus

Concepts associés (18)

Fraction (mathématiques)

Anneau commutatif

Fraction unitaire

Associativité

Associativité des puissances

Afficher plus