Séance de cours

Des produits Lattice au théorème du point fixe de Tarski

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 couvre la combinaison d'éléments de réseau en vecteurs, définissant des ordres partiels, des propriétés d'ordres partiels, des réseaux complets, l'application de théorèmes, des fonctions monotones et le théorème du point fixe de Tarski dans des réseaux complets.

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

Ordre partiel complet

Il existe plusieurs notions non équivalentes dordre partiel complet (complete partial order ou CPO). La notion de CPO est utilisée pour résoudre les équations aux domaines, notamment quand on cherche une sémantique dénotationnelle pour un langage en informatique. Les ensembles partiellement ordonnés ne se comportent pas tous comme des ensembles de parties ordonnés par l'inclusion ⊆. En particulier, quand on a une suite croissante de sous-ensembles E0 ⊆ E1 ⊆ E2 ⊆ ..., on peut définir l'union infinie E0 ∪ E1 ∪ E2 ∪ .

Vecteur euclidien

En mathématiques, et plus précisément en géométrie euclidienne, un vecteur euclidien est un objet géométrique possédant une direction, un sens et une norme. On l'utilise par exemple en physique et en ingénierie pour modéliser une force. On parle aussi parfois de vecteur géométrique dans le plan euclidien (deux dimensions) et de vecteur spatial dans l'espace à trois dimensions. Vecteur#HistoireVecteur En physique et en ingénierie, on travaille souvent dans l'espace euclidien.

Distributive lattice

In mathematics, a distributive lattice is a lattice in which the operations of join and meet distribute over each other. The prototypical examples of such structures are collections of sets for which the lattice operations can be given by set union and intersection. Indeed, these lattices of sets describe the scenery completely: every distributive lattice is—up to isomorphism—given as such a lattice of sets. As in the case of arbitrary lattices, one can choose to consider a distributive lattice L either as a structure of order theory or of universal algebra.

Vecteur

droite|cadre|Deux vecteurs et et leur vecteur somme. En mathématiques, un vecteur est un objet généralisant plusieurs notions provenant de la géométrie (couples de points, translations, etc.), de l'algèbre (« solution » d'un système d'équations à plusieurs inconnues), ou de la physique (forces, vitesses, accélérations). Rigoureusement axiomatisée, la notion de vecteur est le fondement de la branche des mathématiques appelée algèbre linéaire.

Vecteur unitaire

vignette|Deux vecteurs unitaires dans un espace vectoriel normé. Dans un espace vectoriel normé (réel ou complexe) E, un vecteur unitaire est un vecteur dont la norme est égale à 1. Si le corps des scalaires est R, deux vecteurs unitaires v et w sont colinéaires si et seulement si v = w ou v = –w. Si le corps des scalaires est C, et si v est un vecteur unitaire de E, alors les vecteurs unitaires colinéaires à v sont αv où α est un complexe de module 1. Les vecteurs unitaires permettent de définir la direction et le sens d'un vecteur non nul de E.

Afficher plus

Séances de cours associées (64)

Physique 1: Vecteurs et produit à points

Couvre les propriétés des vecteurs, y compris la communativité, la distributivité et la linéarité.

Équations linéaires : vecteurs et matrices

Couvre les équations linéaires, les vecteurs et les matrices, en explorant leurs concepts fondamentaux et leurs applications.

Éléments de groupes de Lie et d'algèbres

Explore la transformation des vecteurs et des tenseurs en physique quantique, en mettant l'accent sur les groupes de Lie et les algèbres.

Vecteurs : Calculs de coordonnées

Couvre les calculs en coordonnées pour les vecteurs, y compris les bases, le produit scalaire et les déterminants, avec des interprétations géométriques et des exemples.

Étude analytique de l'espace

Explore les repères, les coordonnées, les vecteurs, la coplanarité, les équations cartésiennes et les règles géométriques dans l'espace.

Afficher plus

Concepts associés (30)

Ordre partiel complet