Materiály jsou dostupné na webu pedagoga: https://www.cs.vsb.cz/sawa/fvs
Konzultace prostřednictvím MS Teams.
Formální verifikace systémů
| Typ studia | navazující magisterské |
|---|---|
| Jazyk výuky | čeština |
| Kód | 460-4172/01 |
| Zkratka | FVS |
| Název předmětu česky | Formální verifikace systémů |
| Název předmětu anglicky | Formal Verification of Systems |
| Kreditů | 5 |
| Garantující katedra | Katedra informatiky |
| Garant předmětu | doc. Ing. Zdeněk Sawa, Ph.D. |
Osnova předmětu
Přednášky:
- Úvod. Pojem reaktivních systémů, příklady. Přechodové systémy jako základní model.
- Strukturální operační sémantika. Jazyk CCS (Kalkulus komunikujících systémů) pro popis (reaktivních) systémů - syntaxe, sémantika, příklady.
- Behaviorální ekvivalence (tj. pojem ekvivalentního chování systémů). Ekvivalence podle množin běhů (trace equivalence). Silná a slabá bisimulační ekvivalence; bisimulační hry.
- Modální logika HML (Henessy-Milner Logic); popis jednoduchých vlastností chování systému.
- Význam abstraktního pojmu pevného bodu v úplných svazech pro definici sémantiky rekurzivních programů. Výpočet bisimulační ekvivalence jako pevného bodu. HM-logika s rekurzí; charakterizace pomocí her. Korespondence bisimulační ekvivalence a HM-logiky.
- Přechodové systémy s časem. Jazyk CCS s časem (timed CCS) a časované automaty (timed automata).
- Časovaná a nečasovaná bisimulační ekvivalence. Konstrukce regionů a zón u časovaných automatů. TCTL logika pro ověřování modelů (model checking) časovaných systémů.
- Systémy pro interaktivní a automatizované dokazování - Coq jako příklad
takového systému. Základy funkcionálního programování v Coqu.
- Základy logiky v systému Coq. Používání taktik v důkazech. Induktivní definice a důkazy.
- Sémantika programovacích jazyků. Formalizace syntaxe a sémantiky jednoduchého imperativního jazyka.
- Typové systémy. Dokazování vlastností typových systémů.
- Logiky pro dokazování vlastností programů: Hoarova logika a separační logika.
Cvičení:
- Úvod. Pojem reaktivních systémů, příklady. Přechodové systémy jako základní model.
- Strukturální operační sémantika. Jazyk CCS (Kalkulus komunikujících systémů) pro popis (reaktivních) systémů - syntaxe, sémantika, příklady.
- Behaviorální ekvivalence (tj. pojem ekvivalentního chování systémů). Ekvivalence podle množin běhů (trace equivalence). Silná a slabá bisimulační ekvivalence; bisimulační hry.
- Modální logika HML (Henessy-Milner Logic); popis jednoduchých vlastností chování systému.
- Význam abstraktního pojmu pevného bodu v úplných svazech pro definici sémantiky rekurzivních programů. Výpočet bisimulační ekvivalence jako pevného bodu. HM-logika s rekurzí; charakterizace pomocí her. Korespondence bisimulační ekvivalence a HM-logiky.
- Přechodové systémy s časem. Jazyk CCS s časem (timed CCS) a časované automaty (timed automata).
- Časovaná a nečasovaná bisimulační ekvivalence. Konstrukce regionů a zón u časovaných automatů. TCTL logika pro ověřování modelů (model checking) časovaných systémů.
- Systémy pro interaktivní a automatizované dokazování - Coq jako příklad
takového systému. Základy funkcionálního programování v Coqu.
- Základy logiky v systému Coq. Používání taktik v důkazech. Induktivní definice a důkazy.
- Sémantika programovacích jazyků. Formalizace syntaxe a sémantiky jednoduchého imperativního jazyka.
- Typové systémy. Dokazování vlastností typových systémů.
- Logiky pro dokazování vlastností programů: Hoarova logika a separační logika.
- Úvod. Pojem reaktivních systémů, příklady. Přechodové systémy jako základní model.
- Strukturální operační sémantika. Jazyk CCS (Kalkulus komunikujících systémů) pro popis (reaktivních) systémů - syntaxe, sémantika, příklady.
- Behaviorální ekvivalence (tj. pojem ekvivalentního chování systémů). Ekvivalence podle množin běhů (trace equivalence). Silná a slabá bisimulační ekvivalence; bisimulační hry.
- Modální logika HML (Henessy-Milner Logic); popis jednoduchých vlastností chování systému.
- Význam abstraktního pojmu pevného bodu v úplných svazech pro definici sémantiky rekurzivních programů. Výpočet bisimulační ekvivalence jako pevného bodu. HM-logika s rekurzí; charakterizace pomocí her. Korespondence bisimulační ekvivalence a HM-logiky.
- Přechodové systémy s časem. Jazyk CCS s časem (timed CCS) a časované automaty (timed automata).
- Časovaná a nečasovaná bisimulační ekvivalence. Konstrukce regionů a zón u časovaných automatů. TCTL logika pro ověřování modelů (model checking) časovaných systémů.
- Systémy pro interaktivní a automatizované dokazování - Coq jako příklad
takového systému. Základy funkcionálního programování v Coqu.
- Základy logiky v systému Coq. Používání taktik v důkazech. Induktivní definice a důkazy.
- Sémantika programovacích jazyků. Formalizace syntaxe a sémantiky jednoduchého imperativního jazyka.
- Typové systémy. Dokazování vlastností typových systémů.
- Logiky pro dokazování vlastností programů: Hoarova logika a separační logika.
Cvičení:
- Úvod. Pojem reaktivních systémů, příklady. Přechodové systémy jako základní model.
- Strukturální operační sémantika. Jazyk CCS (Kalkulus komunikujících systémů) pro popis (reaktivních) systémů - syntaxe, sémantika, příklady.
- Behaviorální ekvivalence (tj. pojem ekvivalentního chování systémů). Ekvivalence podle množin běhů (trace equivalence). Silná a slabá bisimulační ekvivalence; bisimulační hry.
- Modální logika HML (Henessy-Milner Logic); popis jednoduchých vlastností chování systému.
- Význam abstraktního pojmu pevného bodu v úplných svazech pro definici sémantiky rekurzivních programů. Výpočet bisimulační ekvivalence jako pevného bodu. HM-logika s rekurzí; charakterizace pomocí her. Korespondence bisimulační ekvivalence a HM-logiky.
- Přechodové systémy s časem. Jazyk CCS s časem (timed CCS) a časované automaty (timed automata).
- Časovaná a nečasovaná bisimulační ekvivalence. Konstrukce regionů a zón u časovaných automatů. TCTL logika pro ověřování modelů (model checking) časovaných systémů.
- Systémy pro interaktivní a automatizované dokazování - Coq jako příklad
takového systému. Základy funkcionálního programování v Coqu.
- Základy logiky v systému Coq. Používání taktik v důkazech. Induktivní definice a důkazy.
- Sémantika programovacích jazyků. Formalizace syntaxe a sémantiky jednoduchého imperativního jazyka.
- Typové systémy. Dokazování vlastností typových systémů.
- Logiky pro dokazování vlastností programů: Hoarova logika a separační logika.
E-learning
Povinná literatura
[1] Luca Aceto, Anna Ingólfsdóttir, Kim G. Larsen and Jiří Srba - Reactive Systems: Modelling, Specification and Verification, Cambridge University Press, 2007
[2] Benjamin C. Pierce et al. - Software Foundations (volumes 1 - 5). Electronic textbook, version 6.9.0, 2025. Dostupné na adrese https://softwarefoundations.cis.upenn.edu
[2] Benjamin C. Pierce et al. - Software Foundations (volumes 1 - 5). Electronic textbook, version 6.9.0, 2025. Dostupné na adrese https://softwarefoundations.cis.upenn.edu
Doporučená literatura
[3] Christel Baier, Joost-Pieter Katoen - Principles of Model Checking, The MIT Press, 2008
[4] Béatrice Bérard, Michel Bidoit, Alain Finkel, François Laroussinie, Antoine Petit, Laure Petrucci, Philippe Schnoebelen, Pierre McKenzie - Systems and Software Verification, Springer, 2001
[5] Yves Bertot, Pierre Castéran - Interactive Theorem Proving and Program Development, Springer, 2004.
[6] Andrew W. Appel et al. - Program Logics for Certified Compilers, Cambridge University Press, 2014.
[7] Adam Chlipala - Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant. The MIT Press, 2013.
[8] Benjamin C. Pierce - Types and Programming Languages, MIT Press, 2002.
[9] Benjamin C. Pierce, ed. - Advanced Topics in Types and Programming Languages. MIT Press, 2004.
[10] Glynn Winskel - Formal Semantics of Programming Languages, The MIT Press, 1993.
[11] Hans Hüttel - Transitions and Trees: An Introduction to Structural Operational Semantics, Cambridge University Press, 2010.
[4] Béatrice Bérard, Michel Bidoit, Alain Finkel, François Laroussinie, Antoine Petit, Laure Petrucci, Philippe Schnoebelen, Pierre McKenzie - Systems and Software Verification, Springer, 2001
[5] Yves Bertot, Pierre Castéran - Interactive Theorem Proving and Program Development, Springer, 2004.
[6] Andrew W. Appel et al. - Program Logics for Certified Compilers, Cambridge University Press, 2014.
[7] Adam Chlipala - Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant. The MIT Press, 2013.
[8] Benjamin C. Pierce - Types and Programming Languages, MIT Press, 2002.
[9] Benjamin C. Pierce, ed. - Advanced Topics in Types and Programming Languages. MIT Press, 2004.
[10] Glynn Winskel - Formal Semantics of Programming Languages, The MIT Press, 1993.
[11] Hans Hüttel - Transitions and Trees: An Introduction to Structural Operational Semantics, Cambridge University Press, 2010.