Séance de cours

Assertions auxiliaires 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 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 (25)

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é 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.

Diagramme commutatif

En mathématiques, et plus spécialement dans les applications de la théorie des catégories, un diagramme commutatif est un diagramme d'objets et de morphismes tels que, si l'on suit à travers le diagramme un chemin d'un objet à un autre, le résultat par composition des morphismes ne dépend que de l'objet de départ et de l'objet d'arrivée. Cette définition peut être visualisée par le dessin élémentaire ci-contre. On se place dans la catégorie Ens. Les objets sont les ensembles A, B et C en réalité tous égaux ici à {1,2,3,4}.

Afficher plus

Séances de cours associées (52)

Courbes elliptiques : structure de groupe et isomorphisme

Explore la structure du groupe et l'isomorphisme des courbes elliptiques, y compris les inverses, l'associativité et la compactification du tore.

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.

Opérations associatives: Principes fondamentaux

Couvre les opérations associatives et commutatives dans la programmation parallèle, en utilisant des exemples mathématiques et en discutant des défis dans la préservation de l'associativité.

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.

Afficher plus

Concepts associés (25)

Fraction (mathématiques)

Anneau commutatif

Fraction unitaire

Associativité des puissances

Diagramme commutatif

Afficher plus