Materials will be available in web of the lecturer: https://www.cs.vsb.cz/sawa/fvs-en
Consultations using MS Teams.
Formal Verification of Systems
| Type of study | Follow-up Master |
|---|---|
| Language of instruction | Czech |
| Code | 460-4172/01 |
| Abbreviation | FVS |
| Course title | Formal Verification of Systems |
| Credits | 5 |
| Coordinating department | Department of Computer Science |
| Course coordinator | doc. Ing. Zdeněk Sawa, Ph.D. |
Subject syllabus
Lectures:
- Introduction. Reactive systems, examples. Transition systems as a basic model.
- Structural operational semantics. Language CCS (Calculus of communicating systems) for description of (reactive) system - syntax, semantics, examples.
- Behavioural equivalences (i.e., the notion of equivalent behaviour of systems). Trace equivalence. Strong and weak bisimulation equivalence; bisimulation games.
- Modal logic HML (Henessy-Milner Logic); description of simple properties of behaviour of a system.
- Importance of the abstract notion of fixed point in complete lattices for the definition of semantics of recursive programs. Computation of bisimulation equivalence as a fixed point. HM-logic with recursion; characterization using games. Correspondence between bisimulation equivalence and HM logic.
- Timed transition systems. Timed CCS and timed automata.
- Timed and untimed bisimulation equivalence. Construction of regions and zones for timed automata. Use of TCTL logic for model checking of timed systems.
- Systems for interactive and automated theorem proving. Coq as an example of such system. Basics of functional programming in Coq.
- Basics of logic in Coq. Using tactics in proofs. Inductive definitions and proofs.
- Semantics of programming languages. Formalization of syntax and semantics of a simple imperative programming language.
- Type systems. Proving properties of types systems.
- Logics for proving properties of programs: Hoare logic and separation logic.
Exercises:
- Reactive systems, examples. Transition systems as a basic model.
- Structural operational semantics. Language CCS (Calculus of communicating systems) for description of (reactive) system - syntax, semantics, examples.
- Behavioural equivalences (i.e., the notion of equivalent behaviour of systems). Trace equivalence. Strong and weak bisimulation equivalence; bisimulation games.
- Modal logic HML (Henessy-Milner Logic); description of simple properties of behaviour of a system.
- Importance of the abstract notion of fixed point in complete lattices for the definition of semantics of recursive programs. Computation of bisimulation equivalence as a fixed point. HM-logic with recursion; characterization using games. Correspondence between bisimulation equivalence and HM logic.
- Timed transition systems. Timed CCS and timed automata.
- Timed and untimed bisimulation equivalence. Construction of regions and zones for timed automata. Use of TCTL logic for model checking of timed systems.
- Systems for interactive and automated theorem proving. Coq as an example of such system. Basics of functional programming in Coq.
- Basics of logic in Coq. Using tactics in proofs. Inductive definitions and proofs.
- Semantics of programming languages. Formalization of syntax and semantics of a simple imperative programming language.
- Type systems. Proving properties of types systems.
- Logics for proving properties of programs: Hoare logic and separation logic.
- Introduction. Reactive systems, examples. Transition systems as a basic model.
- Structural operational semantics. Language CCS (Calculus of communicating systems) for description of (reactive) system - syntax, semantics, examples.
- Behavioural equivalences (i.e., the notion of equivalent behaviour of systems). Trace equivalence. Strong and weak bisimulation equivalence; bisimulation games.
- Modal logic HML (Henessy-Milner Logic); description of simple properties of behaviour of a system.
- Importance of the abstract notion of fixed point in complete lattices for the definition of semantics of recursive programs. Computation of bisimulation equivalence as a fixed point. HM-logic with recursion; characterization using games. Correspondence between bisimulation equivalence and HM logic.
- Timed transition systems. Timed CCS and timed automata.
- Timed and untimed bisimulation equivalence. Construction of regions and zones for timed automata. Use of TCTL logic for model checking of timed systems.
- Systems for interactive and automated theorem proving. Coq as an example of such system. Basics of functional programming in Coq.
- Basics of logic in Coq. Using tactics in proofs. Inductive definitions and proofs.
- Semantics of programming languages. Formalization of syntax and semantics of a simple imperative programming language.
- Type systems. Proving properties of types systems.
- Logics for proving properties of programs: Hoare logic and separation logic.
Exercises:
- Reactive systems, examples. Transition systems as a basic model.
- Structural operational semantics. Language CCS (Calculus of communicating systems) for description of (reactive) system - syntax, semantics, examples.
- Behavioural equivalences (i.e., the notion of equivalent behaviour of systems). Trace equivalence. Strong and weak bisimulation equivalence; bisimulation games.
- Modal logic HML (Henessy-Milner Logic); description of simple properties of behaviour of a system.
- Importance of the abstract notion of fixed point in complete lattices for the definition of semantics of recursive programs. Computation of bisimulation equivalence as a fixed point. HM-logic with recursion; characterization using games. Correspondence between bisimulation equivalence and HM logic.
- Timed transition systems. Timed CCS and timed automata.
- Timed and untimed bisimulation equivalence. Construction of regions and zones for timed automata. Use of TCTL logic for model checking of timed systems.
- Systems for interactive and automated theorem proving. Coq as an example of such system. Basics of functional programming in Coq.
- Basics of logic in Coq. Using tactics in proofs. Inductive definitions and proofs.
- Semantics of programming languages. Formalization of syntax and semantics of a simple imperative programming language.
- Type systems. Proving properties of types systems.
- Logics for proving properties of programs: Hoare logic and separation logic.
E-learning
Literature
[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. Available on address https://softwarefoundations.cis.upenn.edu
[2] Benjamin C. Pierce et al. - Software Foundations (volumes 1 - 5). Electronic textbook, version 6.9.0, 2025. Available on address https://softwarefoundations.cis.upenn.edu
Advised literature
[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.