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

Idées de calcul symbolique des États accessibles

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 introduit le concept de calcul symbolique des états accessibles dans les systèmes de transition. Il couvre la définition des systèmes de transition, les propriétés de la fonction G, la séquence des états dans un système de transition et une procédure d'accessibilité en utilisant des points fixes. La séance de cours explique également comment mettre en œuvre la procédure d'accessibilité, un algorithme symbolique, et l'utilisation de formules non normalisées dans le calcul symbolique. L'instructeur discute de la fin des algorithmes pour les systèmes à états finis et de l'importance de simplifier et de normaliser les formules pour éviter une explosion exponentielle.

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

Automate fini

thumb|upright=2|Fig. 1 : Une hiérarchie d'automates. Un automate fini ou automate avec un nombre fini d'états (en anglais finite-state automaton ou finite state machine ou FSM) est un modèle mathématique de calcul, utilisé dans de nombreuses circonstances, allant de la conception de programmes informatiques et de circuits en logique séquentielle aux applications dans des protocoles de communication, en passant par le contrôle des processus, la linguistique et même la biologie.

Automate fini non déterministe

Un automate fini (on dit parfois, par une traduction littérale de l'anglais, machine à états finis, au lieu de machine avec un nombre fini d'états ou machine à états finie ou machine finie à états), finite-state automaton ou finite-state machine (FSA, FSM), est une machine abstraite qui est un outil fondamental en mathématiques discrètes et en informatique. On les retrouve dans la modélisation de processus, le contrôle, les protocoles de communication, la vérification de programmes, la théorie de la calculabilité, dans l'étude des langages formels et en compilation.

Automate fini déterministe

Un automate fini déterministe, parfois abrégé en AFD (en anglais deterministic finite automaton, abrégé en DFA) est un automate fini dont les transitions à partir de chaque état sont déterminées de façon unique par le symbole d'entrée. Un tel automate se distingue ainsi d'un automate fini non déterministe, où au contraire plusieurs possibilités de transitions peuvent exister simultanément pour un état et un symbole d'entrée donné.

Point fixe

En mathématiques, pour une application f d'un ensemble E dans lui-même, un élément x de E est un point fixe de f si f(x) = x. Exemples : dans le plan, la symétrie par rapport à un point A admet un unique point fixe : A ; l'application inverse (définie sur l'ensemble des réels non nuls) admet deux points fixes : –1 et 1, solutions de l'équation équivalente à l'équation . Graphiquement, les points fixes d'une fonction f (d'une variable réelle, à valeurs réelles) sont les points d'intersection de la droite d'équation y = x avec la courbe d'équation y = f(x).

Automate quantique

En informatique quantique et en informatique théorique, un automate fini quantique est une généralisation des automates finis où un mot est accepté selon le résultat d'une certaine mesure. Il existe plusieurs modèles des automates finis quantiques ; le plus restrictif est celui des automates dits « measure-once » de ; un autre est celui des automates « measure-many » de . Ces deux modèles sont très différents l'un de l’autre ; le modèle « measure-once » se rapproche plus de la théorie classique des automates finis.

Afficher plus

Séances de cours associées (42)

Finite Automata: Bases

Introduit les bases des automates finis, y compris les types déterministes et non déterministes, les expressions régulières et les critères d'acceptation.

Expressions régulières (Récapitulatif)

Couvre les principes fondamentaux des expressions régulières et comprend des exercices sur la définition des langues.

Catastrophes et succès des logiciels : Impact de la vérification et systèmes de transition

Explore l'impact de la vérification des logiciels, les catastrophes, les succès et les systèmes de transition.

Mise à l'échelle et renormalisation en mécanique statistique

Explore l'échelle et la renormalisation en mécanique statistique, en mettant l'accent sur les points critiques et les propriétés invariantes.

Catastrophes, succès et invariants inductifs

Explore les catastrophes logicielles, les vérifications réussies, les systèmes de transition et les invariants dans les systèmes.

Afficher plus

Concepts associés (16)

Automate fini

Automate fini non déterministe

Automate fini déterministe

Point fixe

Automate quantique

Afficher plus