110 http://isa.epfl.ch/imoniteur_ISAP/ itffichecours.txt?path=EPFL.Etu.FicheCours.HeaderFR itffichecours.txt?path=EPFL.Etu.FicheCours.GlobalNav_js fr 2026 249847 6683147 249847 2305107546 2305107546 0 0 Informatique IN IC Faculté informatique et communications School of Computer and Communication Sciences !itffichecours.htm?ww_i_matiere=2507044661&ww_x_anneeAcad=2305107546&ww_i_section=249847&ww_i_niveau=6683147 1696552884 1696552963 2024-2025 COURSE BOOKLET CS-550 Formal verification Formal verification Lecturers Kuncak Viktor Language of teaching English Cursus Communication Systems - master program(2024-2025, SC - Master EPFL 2023)
Communication Systems - master program(2024-2025, SC - Master EPFL 2024)
Computer Science - Cybersecurity(2024-2025, IN-CS - Master 2023)
Computer Science - Cybersecurity(2024-2025, IN-CS - Master 2024)
Computer Science(2024-2025, IN - Master 2023)
Computer Science(2024-2025, IN - Master 2024)
Computer and Communication Sciences (edoc)(2024-2025, EDIC 2024-25)
Cyber security minor(2024-2025, Information security minor 2024-25)
Data Science(2024-2025, SC_DS - Master 2023)
Data Science(2024-2025, SC_DS - Master 2024)
SemesterMand.OptionFilières
x
Hx
MA1, MA3x
MA1, MA3xA C D
MA1, MA3xD
 Credits 6 Session Winter Workload 180h Exam During the semester Number of positions Semester Fall Weeks 14 Hours 6 weekly
Courses 2 weekly
Exercises 2 weekly
Project 2 weekly
Study planSemesterMand.OptionFilières
Cyber security 2024-25MA1xD
Cyber security 2024-25MA3xD
Data Science 2024-25MA1x
Data Science 2024-25MA3x
EDIC - Computer and communication sciences 2024-25x
Informatique 2024-25MA1xA C D
Informatique 2024-25MA3xA C D
Mineur : Cyber security 2024-25Hx
Systèmes de communication 2024-25MA1xA C D
Systèmes de communication 2024-25MA3xA C D
Cursus Sem. Type
Computer and Communication Sciences Opt.
Computer science MA1, MA3 Opt.
Cyber security minor H Opt.
Cybersecurity MA1, MA3 Opt.
Data Science MA1, MA3 Opt.
SC master EPFL MA1, MA3 Opt.
Summary 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 the practice behind them. Content

Topics may include (among others) some of the following:

  • Importance of Reliable Systems. Methodology of Formal Verification. Soundness and Completeness in Modeling and Tools. Successful Tools and Flagship Case Studies
  • Review of Sets, Relations, Computability, Propositional and First-Order Logic Syntax, Semantics, Sequent Calculus.
  • Completeness and Semi-Decidability for First-Order Logic. Inductive Definitions and Proof Trees. Higher-Order Logic and LCF Approach.
  • State Machines. Transition Formulas. Traces. Strongest Postconditions and Weakest Preconditions.
  • Hoare Logic. Inductive Invariants. Well-Founded Relations and Termination Measures
  • Linear Temporal Logic. System Verilog Assertions. Monitors
  • SAT Solvers and Bounded Model Checking
  • Model Checking using Binary Decision Diagrams
  • Loop Invariants. Hoare Logic. Statically Checked Function Contracts. Relational Semantics and Fixed-Point Semantics
  • Symbolic Execution. Satisfiability Modulo Theories
  • Abstract Interpretation
  • Set theory for verification
 Learning Prerequisites Recommended courses

CS-320 Computer language processing

 Important concepts to start the course

Discrete Mathematics (e.g. Kenneth Rosen: Discrete Mathematics and Its Applications)

 Learning Outcomes By the end of the course, the student must be able to:
  • Formalize specifications
  • Synthesize loop invariants
  • Specify software functionality
  • Generalize inductive hypothesis
  • Critique current software development practices
 Teaching methods

Instructors will present lectures and exercises and supervise labs on student laptops.

 Expected student activities

Follow the course materials, take mid-term, and complete and explain projects during the semester.

 Assessment methods

The grade is based on the written mid-term, as well as code, documentation, and explanation of projects during the semester. Specific percentages will be communicated in the first class.

 Supervision Office hours Yes Assistants Yes Forum Yes Resources Bibliography
  • Harrison, J. (2009). Handbook of Practical Logic and Automated Reasoning. Cambridge: Cambridge University Press. doi:10.1017/CBO9780511576430
  • Aaron Bradley and Zohar Manna: The Calculus of Computation - Decision Procedures with Applications to Verification, Springer 2007.
  • Michael Huth and Mark Rayan: Logic in Computer Science - Modelling and Reasoning about Systems. Cambridge University Press 2004.
  • Handbook of Model Checking, https://www.springer.com/de/book/9783319105741 Springer 2018. Including Chapter Model Checking Security Protocols by David Basin.
  • Tobias Nipkow, Gerwin Klein: Concrete Semantics with Isabelle/HOL. http://concrete-semantics.org/concrete-semantics.pdf
  • Nielson, Flemming, Nielson, Hanne R., Hankin, Chris: Principles of Program Analysis. ISBN 978-3-662-03811-6. Springer 1999.
  • Peter B. Andrews: An Introduction to Mathematical Logic and Type Theory (To Truth Through Proof), Springer 2002.
  • http://logitext.mit.edu/tutorial
 Ressources en bibliothèque
  • Handbook of Practical Logic and Automated Reasoning / Harrisonhttp://library.epfl.ch/en/beast?isbn=9780521899574
  • Handbook of model checking / Clarkehttp://library.epfl.ch/en/beast?isbn=3-319-10575-2
  • [chapter] Model Checking Security Protocols / Bassinhttps://slsp-epfl.primo.exlibrisgroup.com/permalink/41SLSP_EPF/po9cpk/cdi_springer_books_10_1007_978_3_319_10575_8_22
  • Principles of Program Analysis / Flemminghttp://library.epfl.ch/en/beast?isbn=3-540-65410-0
  • The Calculus of Computation / Bradleyhttp://library.epfl.ch/en/beast?isbn=9783540741138
  • Logic in Computer Science / Huthhttp://library.epfl.ch/en/beast?isbn=0-521-54310-X
  • Introduction to mathematical logic and type theory / Andrews1402007639
 Notes/Handbook

https://lara.epfl.ch/w/fv

Websites Moodle Link Informatique, 2024-2025, Master semestre 1 Computer Science, 2024-2025, Master semester 1 Ecole polytechnique fédérale de Lausanne EPFL Ecole polytechnique fédérale de Lausanne EPFL 2024-2025 Master semestre 1 MA1 HIVER Master semester 1 MA1 Informatique IN Computer Science IN
Informatique IN Computer Science IN
A C D optionnel optional
2 Cours Courses Heure(s) hebdo x 14 semaines Hour(s) per week x 14 weeks H hebdo H hebdo Kuncak Viktor 177241
Informatique IN Computer Science IN
2 Exercices Exercises Heure(s) hebdo x 14 semaines Hour(s) per week x 14 weeks H hebdo H hebdo Kuncak Viktor 177241
Informatique IN Computer Science IN
2 Projet Project Heure(s) hebdo x 14 semaines Hour(s) per week x 14 weeks H hebdo H hebdo Kuncak Viktor 177241
Informatique IN Computer Science IN
2507044661 Formal verification Formal verification 6
Pendant le semestre During the semester Crédit Credits 6 Session hiver Session winter HIV HIV
Informatique, 2024-2025, Master semestre 3 Computer Science, 2024-2025, Master semester 3 Ecole polytechnique fédérale de Lausanne EPFL Ecole polytechnique fédérale de Lausanne EPFL 2024-2025 Master semestre 3 MA3 HIVER Master semester 3 MA3 Informatique IN Computer Science IN
Informatique IN Computer Science IN
A C D optionnel optional
2 Cours Courses Heure(s) hebdo x 14 semaines Hour(s) per week x 14 weeks H hebdo H hebdo Kuncak Viktor 177241
Informatique IN Computer Science IN
2 Exercices Exercises Heure(s) hebdo x 14 semaines Hour(s) per week x 14 weeks H hebdo H hebdo Kuncak Viktor 177241
Informatique IN Computer Science IN
2 Projet Project Heure(s) hebdo x 14 semaines Hour(s) per week x 14 weeks H hebdo H hebdo Kuncak Viktor 177241
Informatique IN Computer Science IN
2507044661 Formal verification Formal verification 6
Pendant le semestre During the semester Crédit Credits 6 Session hiver Session winter HIV HIV
Data Science, 2024-2025, Master semestre 1 Data Science, 2024-2025, Master semester 1 Ecole polytechnique fédérale de Lausanne EPFL Ecole polytechnique fédérale de Lausanne EPFL 2024-2025 Master semestre 1 MA1 HIVER Master semester 1 MA1 Data Science SC_DS Data Science SC_DS
Systèmes de communication SC Communication Systems SC
optionnel optional
2 Cours Courses Heure(s) hebdo x 14 semaines Hour(s) per week x 14 weeks H hebdo H hebdo Kuncak Viktor 177241
Informatique IN Computer Science IN
2 Exercices Exercises Heure(s) hebdo x 14 semaines Hour(s) per week x 14 weeks H hebdo H hebdo Kuncak Viktor 177241
Informatique IN Computer Science IN
2 Projet Project Heure(s) hebdo x 14 semaines Hour(s) per week x 14 weeks H hebdo H hebdo Kuncak Viktor 177241
Informatique IN Computer Science IN
2507044661 Formal verification Formal verification 6
Pendant le semestre During the semester Crédit Credits 6 Session hiver Session winter HIV HIV
Data Science, 2024-2025, Master semestre 3 Data Science, 2024-2025, Master semester 3 Ecole polytechnique fédérale de Lausanne EPFL Ecole polytechnique fédérale de Lausanne EPFL 2024-2025 Master semestre 3 MA3 HIVER Master semester 3 MA3 Data Science SC_DS Data Science SC_DS
Systèmes de communication SC Communication Systems SC
optionnel optional
2 Cours Courses Heure(s) hebdo x 14 semaines Hour(s) per week x 14 weeks H hebdo H hebdo Kuncak Viktor 177241
Informatique IN Computer Science IN
2 Exercices Exercises Heure(s) hebdo x 14 semaines Hour(s) per week x 14 weeks H hebdo H hebdo Kuncak Viktor 177241
Informatique IN Computer Science IN
2 Projet Project Heure(s) hebdo x 14 semaines Hour(s) per week x 14 weeks H hebdo H hebdo Kuncak Viktor 177241
Informatique IN Computer Science IN
2507044661 Formal verification Formal verification 6
Pendant le semestre During the semester Crédit Credits 6 Session hiver Session winter HIV HIV
Informatique - Cybersecurity, 2024-2025, Master semestre 1 Computer Science - Cybersecurity, 2024-2025, Master semester 1 Ecole polytechnique fédérale de Lausanne EPFL Ecole polytechnique fédérale de Lausanne EPFL 2024-2025 Master semestre 1 MA1 HIVER Master semester 1 MA1 Informatique - Cybersecurity IN_CS Computer Science - Cybersecurity IN_CS
Informatique IN Computer Science IN
D optionnel optional
2 Cours Courses Heure(s) hebdo x 14 semaines Hour(s) per week x 14 weeks H hebdo H hebdo Kuncak Viktor 177241
Informatique IN Computer Science IN
2 Exercices Exercises Heure(s) hebdo x 14 semaines Hour(s) per week x 14 weeks H hebdo H hebdo Kuncak Viktor 177241
Informatique IN Computer Science IN
2 Projet Project Heure(s) hebdo x 14 semaines Hour(s) per week x 14 weeks H hebdo H hebdo Kuncak Viktor 177241
Informatique IN Computer Science IN
2507044661 Formal verification Formal verification 6
Pendant le semestre During the semester Crédit Credits 6 Session hiver Session winter HIV HIV
Informatique - Cybersecurity, 2024-2025, Master semestre 3 Computer Science - Cybersecurity, 2024-2025, Master semester 3 Ecole polytechnique fédérale de Lausanne EPFL Ecole polytechnique fédérale de Lausanne EPFL 2024-2025 Master semestre 3 MA3 HIVER Master semester 3 MA3 Informatique - Cybersecurity IN_CS Computer Science - Cybersecurity IN_CS
Informatique IN Computer Science IN
D optionnel optional
2 Cours Courses Heure(s) hebdo x 14 semaines Hour(s) per week x 14 weeks H hebdo H hebdo Kuncak Viktor 177241
Informatique IN Computer Science IN
2 Exercices Exercises Heure(s) hebdo x 14 semaines Hour(s) per week x 14 weeks H hebdo H hebdo Kuncak Viktor 177241
Informatique IN Computer Science IN
2 Projet Project Heure(s) hebdo x 14 semaines Hour(s) per week x 14 weeks H hebdo H hebdo Kuncak Viktor 177241
Informatique IN Computer Science IN
2507044661 Formal verification Formal verification 6
Pendant le semestre During the semester Crédit Credits 6 Session hiver Session winter HIV HIV
Systèmes de communication - master, 2024-2025, Master semestre 1 Communication Systems - master program, 2024-2025, Master semester 1 Ecole polytechnique fédérale de Lausanne EPFL Ecole polytechnique fédérale de Lausanne EPFL 2024-2025 Master semestre 1 MA1 HIVER Master semester 1 MA1 Systèmes de communication - master SC_EPFL Communication Systems - master program SC_EPFL
Systèmes de communication SC Communication Systems SC
A C D optionnel optional
2 Cours Courses Heure(s) hebdo x 14 semaines Hour(s) per week x 14 weeks H hebdo H hebdo Kuncak Viktor 177241
Informatique IN Computer Science IN
2 Exercices Exercises Heure(s) hebdo x 14 semaines Hour(s) per week x 14 weeks H hebdo H hebdo Kuncak Viktor 177241
Informatique IN Computer Science IN
2 Projet Project Heure(s) hebdo x 14 semaines Hour(s) per week x 14 weeks H hebdo H hebdo Kuncak Viktor 177241
Informatique IN Computer Science IN
2507044661 Formal verification Formal verification 6
Pendant le semestre During the semester Crédit Credits 6 Session hiver Session winter HIV HIV
Systèmes de communication - master, 2024-2025, Master semestre 3 Communication Systems - master program, 2024-2025, Master semester 3 Ecole polytechnique fédérale de Lausanne EPFL Ecole polytechnique fédérale de Lausanne EPFL 2024-2025 Master semestre 3 MA3 HIVER Master semester 3 MA3 Systèmes de communication - master SC_EPFL Communication Systems - master program SC_EPFL
Systèmes de communication SC Communication Systems SC
A C D optionnel optional
2 Cours Courses Heure(s) hebdo x 14 semaines Hour(s) per week x 14 weeks H hebdo H hebdo Kuncak Viktor 177241
Informatique IN Computer Science IN
2 Exercices Exercises Heure(s) hebdo x 14 semaines Hour(s) per week x 14 weeks H hebdo H hebdo Kuncak Viktor 177241
Informatique IN Computer Science IN
2 Projet Project Heure(s) hebdo x 14 semaines Hour(s) per week x 14 weeks H hebdo H hebdo Kuncak Viktor 177241
Informatique IN Computer Science IN
2507044661 Formal verification Formal verification 6
Pendant le semestre During the semester Crédit Credits 6 Session hiver Session winter HIV HIV
Cyber security minor, 2024-2025, Semestre automne Cyber security minor, 2024-2025, Autumn semester Ecole polytechnique fédérale de Lausanne EPFL Ecole polytechnique fédérale de Lausanne EPFL 2024-2025 Semestre automne H HIVER Autumn semester H Cyber security minor MIN_IN_SEC Cyber security minor MIN_IN_SEC
optionnel optional
2 Cours Courses Heure(s) hebdo x 14 semaines Hour(s) per week x 14 weeks H hebdo H hebdo Kuncak Viktor 177241
Informatique IN Computer Science IN
2 Exercices Exercises Heure(s) hebdo x 14 semaines Hour(s) per week x 14 weeks H hebdo H hebdo Kuncak Viktor 177241
Informatique IN Computer Science IN
2 Projet Project Heure(s) hebdo x 14 semaines Hour(s) per week x 14 weeks H hebdo H hebdo Kuncak Viktor 177241
Informatique IN Computer Science IN
2507044661 Formal verification Formal verification 6
Pendant le semestre During the semester Crédit Credits 6 Session hiver Session winter HIV HIV
Informatique et communications (edoc), 2024-2025 Computer and Communication Sciences (edoc), 2024-2025 Ecole polytechnique fédérale de Lausanne EPFL Ecole polytechnique fédérale de Lausanne EPFL 2024-2025 Informatique et communications (edoc) EDIC Computer and Communication Sciences (edoc) EDIC
optionnel optional
2 Cours Courses Heure(s) hebdo x 14 semaines Hour(s) per week x 14 weeks H hebdo H hebdo Kuncak Viktor 177241
Informatique IN Computer Science IN
2 Exercices Exercises Heure(s) hebdo x 14 semaines Hour(s) per week x 14 weeks H hebdo H hebdo Kuncak Viktor 177241
Informatique IN Computer Science IN
2 Projet Project Heure(s) hebdo x 14 semaines Hour(s) per week x 14 weeks H hebdo H hebdo Kuncak Viktor 177241
Informatique IN Computer Science IN
2507044661 Formal verification Formal verification 6
Pendant le semestre During the semester Crédit Credits 6 Session hiver Session winter HIV HIV
BALISES_TEXTES BOOLEAN_Symbol BaliseJS_debut BaliseJS_fin Balise_debut Balise_fin FO_debut FO_fin HTML_debut HTML_fin JS_debut JS_fin BALISE_BOLD BOOLEAN_Symbol BaliseJS_debut \x5bb\x5d BaliseJS_fin \x5b\x2fb\x5d Balise_debut [b] Balise_fin [/b] FO_debut font-weight=bold FO_fin font-weight=normal HTML_debut <b> HTML_fin </b> JS_debut \x3cb\x3e JS_fin \x3c\x2fb\x3e BALISE_ITALIC BOOLEAN_Symbol BaliseJS_debut \x5bi\x5d BaliseJS_fin \x5b\x2fi\x5d Balise_debut [i] Balise_fin [/i] FO_debut font-style=italic FO_fin font-style=normal HTML_debut <i> HTML_fin </i> JS_debut \x3ci\x3e JS_fin \x3c\x2fi\x3e BALISE_RED BOOLEAN_Symbol BaliseJS_debut \x5bred\x5d BaliseJS_fin \x5b\x2fred\x5d Balise_debut [red] Balise_fin [/red] FO_debut color=#990033 FO_fin color=black HTML_debut <span style="color:#990033;"> HTML_fin </span> JS_debut \x3cspan style="color:#990033;"\x3e JS_fin \x3c\x2fspan\x3e BALISE_TAB BOOLEAN_Symbol BaliseJS_debut \x5btab\x5d BaliseJS_fin Balise_debut [tab] Balise_fin FO_debut [inline]=&#160;&#160;&#160;&#160;&#160;&#160;&#160;&#160; FO_fin HTML_debut <img src="/images/gestacplus/base/pixel.gif" width="40" height="1"/> HTML_fin JS_debut \x3cimg src="\x2fimages\x2fgestacplus\x2fbase\x2fpixel.gif" width="40" height="1"\x2f\x3e JS_fin BALISE_LIST BOOLEAN_Symbol BaliseJS_debut \x5bli\x5d BaliseJS_fin Balise_debut [li] Balise_fin FO_debut [inline]=&#x2022;&#160;&#160; FO_fin HTML_debut &#x2022;&#160;&#160; HTML_fin JS_debut \x26#x2022;\x26#160;\x26#160; JS_fin CODE5045487 BOOLEAN_Symbol BaliseJS_debut \x5b\x5d BaliseJS_fin Balise_debut [] Balise_fin FO_debut [inline]=&#160; FO_fin HTML_debut &#160; HTML_fin JS_debut \x26#160; JS_fin BALISE_GREEN BOOLEAN_Symbol BaliseJS_debut \x5bgreen\x5d BaliseJS_fin \x5b\x2fgreen\x5d Balise_debut [green] Balise_fin [/green] FO_debut color=#008000 FO_fin color=black HTML_debut <span style="color:#008000;"> HTML_fin </span> JS_debut \x3cspan style="color:#008000;"\x3e JS_fin \x3c\x2fspan\x3e CODE7508550 BOOLEAN_Symbol BaliseJS_debut \x5bblue\x5d BaliseJS_fin \x5b\x2fblue\x5d Balise_debut [blue] Balise_fin [/blue] FO_debut color=#0080FF FO_fin color=black HTML_debut <span style="color:#0080FF;"> HTML_fin </span> JS_debut \x3cspan style="color:#0080FF;"\x3e JS_fin \x3c\x2fspan\x3e BALISE_COURIER BOOLEAN_Symbol BaliseJS_debut \x5bcourier\x5d BaliseJS_fin \x5b\x2fcourier\x5d Balise_debut [courier] Balise_fin [/courier] FO_debut font-family=Courier FO_fin font-family= HTML_debut <font style="font-family:Courier;"> HTML_fin </font> JS_debut \x3cfont style="font-family:Courier;"\x3e JS_fin \x3c\x2ffont\x3e BALISE_SIZE20 BOOLEAN_Symbol BaliseJS_debut \x5b20\x5d BaliseJS_fin \x5b\x2f20\x5d Balise_debut [20] Balise_fin [/20] FO_debut font-size=20pt FO_fin font-size= HTML_debut <font style="font-size:20pt;"> HTML_fin </font> JS_debut \x3cfont style="font-size:20pt;"\x3e JS_fin \x3c\x2ffont\x3e BALISE_SIZE16 BOOLEAN_Symbol BaliseJS_debut \x5b16\x5d BaliseJS_fin \x5b\x2f16\x5d Balise_debut [16] Balise_fin [/16] FO_debut font-size=16pt FO_fin font-size= HTML_debut <font style="font-size:16pt;"> HTML_fin </font> JS_debut \x3cfont style="font-size:16pt;"\x3e JS_fin \x3c\x2ffont\x3e BALISE_SIZE12 BOOLEAN_Symbol BaliseJS_debut \x5b12\x5d BaliseJS_fin \x5b\x2f12\x5d Balise_debut [12] Balise_fin [/12] FO_debut font-size=12pt FO_fin font-size= HTML_debut <font style="font-size:12pt;"> HTML_fin </font> JS_debut \x3cfont style="font-size:12pt;"\x3e JS_fin \x3c\x2ffont\x3e BALISE_SIZE8 BOOLEAN_Symbol BaliseJS_debut \x5b8\x5d BaliseJS_fin \x5b\x2f8\x5d Balise_debut [8] Balise_fin [/8] FO_debut font-size=8pt FO_fin font-size= HTML_debut <font style="font-size:8pt;"> HTML_fin </font> JS_debut \x3cfont style="font-size:8pt;"\x3e JS_fin \x3c\x2ffont\x3e BALISE_BLACKBACK BOOLEAN_Symbol BaliseJS_debut \x5bblackback\x5d BaliseJS_fin \x5b\x2fblackback\x5d Balise_debut [blackback] Balise_fin [/blackback] FO_debut background-color=black FO_fin background-color=white HTML_debut <span style="background-color:black;"> HTML_fin </span> JS_debut \x3cspan style="background-color:black;"\x3e JS_fin \x3c\x2fspan\x3e BALISE_WHITE BOOLEAN_Symbol BaliseJS_debut \x5bwhite\x5d BaliseJS_fin \x5b\x2fwhite\x5d Balise_debut [white] Balise_fin [/white] FO_debut color=white FO_fin color=black HTML_debut <span style="color:white;"> HTML_fin </span> JS_debut \x3cspan style="color:white;"\x3e JS_fin \x3c\x2fspan\x3e CODE47534071 BOOLEAN_Symbol 1 BaliseJS_debut \x5bbeta\x5d BaliseJS_fin Balise_debut [beta] Balise_fin FO_debut [inline]=&#946; FO_fin HTML_debut &#946; HTML_fin JS_debut \x26#946; JS_fin CODE47534435 BOOLEAN_Symbol 1 BaliseJS_debut \x5balpha\x5d BaliseJS_fin Balise_debut [alpha] Balise_fin FO_debut [inline]=&#945; FO_fin HTML_debut &#945; HTML_fin JS_debut \x26#945; JS_fin CODE47551722 BOOLEAN_Symbol BaliseJS_debut \x5bsub\x5d BaliseJS_fin \x5b\x2fsub\x5d Balise_debut [sub] Balise_fin [/sub] FO_debut vertical-align=sub FO_fin vertical-align=baseline HTML_debut <sub> HTML_fin </sub> JS_debut \x3csub\x3e JS_fin \x3c\x2fsub\x3e CODE48535424 BOOLEAN_Symbol 1 BaliseJS_debut \x5bLAMBDA\x5d BaliseJS_fin Balise_debut [LAMBDA] Balise_fin FO_debut [inline]=&#923; FO_fin HTML_debut &#923; HTML_fin JS_debut \x26#923; JS_fin CODE48535666 BOOLEAN_Symbol 1 BaliseJS_debut \x5blambda\x5d BaliseJS_fin Balise_debut [lambda] Balise_fin FO_debut [inline]=&#955; FO_fin HTML_debut &#955; HTML_fin JS_debut \x26#955; JS_fin CODE47551793 BOOLEAN_Symbol BaliseJS_debut \x5bsup\x5d BaliseJS_fin \x5b\x2fsup\x5d Balise_debut [sup] Balise_fin [/sup] FO_debut vertical-align=super FO_fin vertical-align=baseline HTML_debut <sup> HTML_fin </sup> JS_debut \x3csup\x3e JS_fin \x3c\x2fsup\x3e CODE56031535 BOOLEAN_Symbol 1 BaliseJS_debut \x5bdelta\x5d BaliseJS_fin Balise_debut [delta] Balise_fin FO_debut [inline]=&#948; FO_fin HTML_debut &#948; HTML_fin JS_debut \x26#948; JS_fin CODE56073309 BOOLEAN_Symbol 1 BaliseJS_debut \x5bpi\x5d BaliseJS_fin Balise_debut [pi] Balise_fin FO_debut [inline]=&#960; FO_fin HTML_debut &#960; HTML_fin JS_debut \x26#960; JS_fin CODE56074095 BOOLEAN_Symbol 1 BaliseJS_debut \x5bDELTA\x5d BaliseJS_fin Balise_debut [DELTA] Balise_fin FO_debut [inline]=&#916; FO_fin HTML_debut &#916; HTML_fin JS_debut \x26#916; JS_fin CODE56074172 BOOLEAN_Symbol 1 BaliseJS_debut \x5bMU\x5d BaliseJS_fin Balise_debut [MU] Balise_fin FO_debut [inline]=&#924; FO_fin HTML_debut &#924; HTML_fin JS_debut \x26#924; JS_fin CODE56074264 BOOLEAN_Symbol 1 BaliseJS_debut \x5bPI\x5d BaliseJS_fin Balise_debut [PI] Balise_fin FO_debut [inline]=&#928; FO_fin HTML_debut &#928; HTML_fin JS_debut \x26#928; JS_fin CODE56074328 BOOLEAN_Symbol 1 BaliseJS_debut \x5bSIGMA\x5d BaliseJS_fin Balise_debut [SIGMA] Balise_fin FO_debut [inline]=&#931; FO_fin HTML_debut &#931; HTML_fin JS_debut \x26#931; JS_fin CODE56075056 BOOLEAN_Symbol 1 BaliseJS_debut \x5bALPHA\x5d BaliseJS_fin Balise_debut [ALPHA] Balise_fin FO_debut [inline]=&#913; FO_fin HTML_debut &#913; HTML_fin JS_debut \x26#913; JS_fin CODE56075186 BOOLEAN_Symbol 1 BaliseJS_debut \x5bBETA\x5d BaliseJS_fin Balise_debut [BETA] Balise_fin FO_debut [inline]=&#914; FO_fin HTML_debut &#914; HTML_fin JS_debut \x26#914; JS_fin BALISE_SYMBOL BOOLEAN_Symbol BaliseJS_debut \x5bsymbol\x5d BaliseJS_fin \x5b\x2fsymbol\x5d Balise_debut [symbol] Balise_fin [/symbol] FO_debut font-family=Symbol FO_fin font-family= HTML_debut <font style="font-family:Symbol;"> HTML_fin </font> JS_debut \x3cfont style="font-family:Symbol;"\x3e JS_fin \x3c\x2ffont\x3e CODE56072935 BOOLEAN_Symbol 1 BaliseJS_debut \x5bmu\x5d BaliseJS_fin Balise_debut [mu] Balise_fin FO_debut [inline]=&#956; FO_fin HTML_debut &#956; HTML_fin JS_debut \x26#956; JS_fin CODE56073842 BOOLEAN_Symbol 1 BaliseJS_debut \x5bsigma\x5d BaliseJS_fin Balise_debut [sigma] Balise_fin FO_debut [inline]=&#963; FO_fin HTML_debut &#963; HTML_fin JS_debut \x26#963; JS_fin CODE68199232 BOOLEAN_Symbol 1 BaliseJS_debut \x5bphi\x5d BaliseJS_fin Balise_debut [phi] Balise_fin FO_debut [inline]=&#966; FO_fin HTML_debut &#966; HTML_fin JS_debut \x26#966; JS_fin CODE68199285 BOOLEAN_Symbol 1 BaliseJS_debut \x5bPHI\x5d BaliseJS_fin Balise_debut [PHI] Balise_fin FO_debut [inline]=&#934; FO_fin HTML_debut &#934; HTML_fin JS_debut \x26#934; JS_fin CODE68199991 BOOLEAN_Symbol 1 BaliseJS_debut \x5bgamma\x5d BaliseJS_fin Balise_debut [gamma] Balise_fin FO_debut [inline]=&#947; FO_fin HTML_debut &#947; HTML_fin JS_debut \x26#947; JS_fin CODE68200031 BOOLEAN_Symbol 1 BaliseJS_debut \x5bGAMMA\x5d BaliseJS_fin Balise_debut [GAMMA] Balise_fin FO_debut [inline]=&#915; FO_fin HTML_debut &#915; HTML_fin JS_debut \x26#915; JS_fin CODE68200077 BOOLEAN_Symbol 1 BaliseJS_debut \x5bomega\x5d BaliseJS_fin Balise_debut [omega] Balise_fin FO_debut [inline]=&#969; FO_fin HTML_debut &#969; HTML_fin JS_debut \x26#969; JS_fin CODE68200150 BOOLEAN_Symbol 1 BaliseJS_debut \x5bOMEGA\x5d BaliseJS_fin Balise_debut [OMEGA] Balise_fin FO_debut [inline]=&#937; FO_fin HTML_debut &#937; HTML_fin JS_debut \x26#937; JS_fin CODE72092691 BOOLEAN_Symbol BaliseJS_debut \x5beta\x5d BaliseJS_fin Balise_debut [eta] Balise_fin FO_debut [inline]=&#951; FO_fin HTML_debut &#951; HTML_fin JS_debut \x26#951; JS_fin CODE72092805 BOOLEAN_Symbol BaliseJS_debut \x5bETA\x5d BaliseJS_fin Balise_debut [ETA] Balise_fin FO_debut [inline]=&#919; FO_fin HTML_debut &#919; HTML_fin JS_debut \x26#919; JS_fin BALISE_SOULIGNER BOOLEAN_Symbol BaliseJS_debut \x5bu\x5d BaliseJS_fin \x5b\x2fu\x5d Balise_debut [u] Balise_fin [/u] FO_debut text-decoration=underline FO_fin text-decoration=none HTML_debut <u> HTML_fin </u> JS_debut \x3cu\x3e JS_fin \x3c\x2fu\x3e CODE72092388 BOOLEAN_Symbol BaliseJS_debut \x5bpsi\x5d BaliseJS_fin Balise_debut [psi] Balise_fin FO_debut [inline]=&#968; FO_fin HTML_debut &#968; HTML_fin JS_debut \x26#968; JS_fin CODE72092541 BOOLEAN_Symbol BaliseJS_debut \x5bPSI\x5d BaliseJS_fin Balise_debut [PSI] Balise_fin FO_debut [inline]=&#936; FO_fin HTML_debut &#936; HTML_fin JS_debut \x26#936; JS_fin CODE140502511 BOOLEAN_Symbol 1 BaliseJS_debut \x5brho\x5d BaliseJS_fin Balise_debut [rho] Balise_fin FO_debut [inline]=&#961; FO_fin HTML_debut &#961; HTML_fin JS_debut \x26#961; JS_fin CODE140504636 BOOLEAN_Symbol 1 BaliseJS_debut \x5bRHO\x5d BaliseJS_fin Balise_debut [RHO] Balise_fin FO_debut [inline]=&#929; FO_fin HTML_debut &#929; HTML_fin JS_debut \x26#929; JS_fin CODE148292791 BOOLEAN_Symbol BaliseJS_debut \x5bepsilon\x5d BaliseJS_fin Balise_debut [epsilon] Balise_fin FO_debut [inline]=&#949; FO_fin HTML_debut &#949; HTML_fin JS_debut \x26#949; JS_fin CODE169976220 BOOLEAN_Symbol BaliseJS_debut \x5blig\x5d BaliseJS_fin Balise_debut [lig] Balise_fin FO_debut [inline]=&#x203A;&#160;&#160; FO_fin HTML_debut &#x203A;&#160;&#160; HTML_fin JS_debut \x26#x203A;\x26#160;\x26#160; JS_fin CODE148292899 BOOLEAN_Symbol BaliseJS_debut \x5bEPSILON\x5d BaliseJS_fin Balise_debut [EPSILON] Balise_fin FO_debut [inline]=&#917; FO_fin HTML_debut &#917; HTML_fin JS_debut \x26#917; JS_fin BALISETXT_SAUT BOOLEAN_Symbol BaliseJS_debut \x5bbr\x2f\x5d BaliseJS_fin Balise_debut [br/] Balise_fin FO_debut FO_fin HTML_debut <br/> HTML_fin JS_debut \x3cbr\x2f\x3e JS_fin 2507044661 Formal verification Formal verification anglais Kuncak Viktor 177241 2483907795