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

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

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

Treillis (ensemble ordonné)

En mathématiques, un treillis () est une des structures algébriques utilisées en algèbre générale. C'est un ensemble partiellement ordonné dans lequel chaque paire d'éléments admet une borne supérieure et une borne inférieure. Un treillis peut être vu comme le treillis de Galois d'une relation binaire. Il existe en réalité deux définitions équivalentes du treillis, une concernant la relation d'ordre citée précédemment, l'autre algébrique. Tout ensemble muni d'une relation d'ordre total est un treillis.

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

Complete lattice

In mathematics, a complete lattice is a partially ordered set in which all subsets have both a supremum (join) and an infimum (meet). A lattice which satisfies at least one of these properties is known as a conditionally complete lattice. Specifically, every non-empty finite lattice is complete. Complete lattices appear in many applications in mathematics and computer science. Being a special instance of lattices, they are studied both in order theory and universal algebra.

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.

Completeness (order theory)

In the mathematical area of order theory, completeness properties assert the existence of certain infima or suprema of a given partially ordered set (poset). The most familiar example is the completeness of the real numbers. A special use of the term refers to complete partial orders or complete lattices. However, many other interesting notions of completeness exist. The motivation for considering completeness properties derives from the great importance of suprema (least upper bounds, joins, "") and infima (greatest lower bounds, meets, "") to the theory of partial orders.

Afficher plus

Séances de cours associées (32)

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

Vector Transformation et Tension

Explore la transformation des vecteurs et des tenseurs, y compris les rotations et les représentations en physique quantique.

Notation Indicielle et Vecteurs

Explore la notation indicielle, les vecteurs et la loi de transformation dans le contexte de la densité de flux de masse.

Calculus vectoriaux : scalaires et vectoriaux

Introduit des scalars et des vecteurs, expliquant leurs propriétés et les opérations mathématiques.

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.

Afficher plus

Concepts associés (28)

Treillis (ensemble ordonné)

Ordre partiel complet

Complete lattice

Vecteur euclidien

Completeness (order theory)

Afficher plus