IA159 Formal Methods for Software Analysis

Fakulta informatiky
podzim 2024
Rozsah
2/0/0. 2 kr. (plus ukončení). Ukončení: zk.
Vyučováno kontaktně
Vyučující
prof. RNDr. Jan Strejček, Ph.D. (přednášející)
Garance
prof. RNDr. Jan Strejček, Ph.D.
Katedra teorie programování – Fakulta informatiky
Dodavatelské pracoviště: Katedra teorie programování – Fakulta informatiky
Rozvrh
St 25. 9. až St 18. 12. St 10:00–11:50 A217
Předpoklady
Some degree of abstract math reasoning.
Omezení zápisu do předmětu
Předmět je nabízen i studentům mimo mateřské obory.
Mateřské obory/plány
předmět má 29 mateřských oborů, zobrazit
Cíle předmětu
At the end of this course, students should understand and be able to explain principles and applications of basic and selected advanced formal methods for software analysis. Students should be also able to make reasoned decisions about suitability of various methods for given goals and to apply suitable formal methods or tools.
Výstupy z učení
At the end of this course, students should understand and be able to explain principles and applications of basic and selected advanced formal methods for software analysis. Students should be also able to make reasoned decisions about suitability of various methods for given goals and to apply suitable formal methods or tools.
Osnova
  • Formal aspects of testing (coverage criteria, software quality metrics).
  • Automated test generation: greybox fuzzing.
  • Deductive verification.
  • Static analysis and abstract interpretation.
  • Points-to analysis, control and data dependencies, program slicing.
  • Shape analysis.
  • Symbolic execution and bounded model checking, concolic execution, whitebox fuzz testing.
  • Configurable program analysis.
  • Verification via automata, symbolic execution, and Interpolation.
  • Verification witnesses.
Literatura
  • PELED, Doron A. Software reliability methods. New York: Springer, 2001, xix, 331. ISBN 0387951067. info
  • CLARKE, E. M., Orna GRUMBERG, Doron PELED, Daniel KROENING a Helmut VEITH. Model checking. Second edition. Cambridge, Massachusetts: MIT Press, 2018, xx, 402. ISBN 9780262038836. info
  • Handbook of model checking. Edited by E. M. Clarke - T. A. Henzinger - Helmut Veith - Roderick Bloem. Cham: Springer International Publishing AG, 2018, xxiv, 1210. ISBN 9783319105741. info
Výukové metody
lectures
Metody hodnocení
oral exam
Vyučovací jazyk
Angličtina
Další komentáře
Studijní materiály
Předmět je vyučován každoročně.
Předmět je zařazen také v obdobích jaro 2008, jaro 2009, jaro 2010, jaro 2011, jaro 2012, jaro 2013, jaro 2014, jaro 2015, jaro 2016, jaro 2017, jaro 2018, jaro 2019, jaro 2020, jaro 2021, jaro 2022, jaro 2023, podzim 2023.

IA159 Formal Methods for Software Analysis

Fakulta informatiky
podzim 2023
Rozsah
2/0/0. 2 kr. (plus ukončení). Ukončení: zk.
Vyučující
prof. RNDr. Jan Strejček, Ph.D. (přednášející)
Garance
prof. RNDr. Jan Strejček, Ph.D.
Katedra teorie programování – Fakulta informatiky
Dodavatelské pracoviště: Katedra teorie programování – Fakulta informatiky
Rozvrh
Čt 12:00–13:50 A319
Předpoklady
Some degree of abstract math reasoning.
Omezení zápisu do předmětu
Předmět je nabízen i studentům mimo mateřské obory.
Mateřské obory/plány
předmět má 49 mateřských oborů, zobrazit
Cíle předmětu
At the end of this course, students should understand and be able to explain principles and applications of basic and selected advanced formal methods for software analysis. Students should be also able to make reasoned decisions about suitability of various methods for given goals and to apply suitable formal methods or tools.
Výstupy z učení
At the end of this course, students should understand and be able to explain principles and applications of basic and selected advanced formal methods for software analysis. Students should be also able to make reasoned decisions about suitability of various methods for given goals and to apply suitable formal methods or tools.
Osnova
  • Formal aspects of testing (coverage criteria, software quality metrics).
  • Automated test generation: greybox fuzzing.
  • Deductive verification.
  • Static analysis and abstract interpretation.
  • Points-to analysis, control and data dependencies, program slicing.
  • Shape analysis.
  • Symbolic execution and bounded model checking, concolic execution, whitebox fuzz testing.
  • Configurable program analysis.
  • Verification via automata, symbolic execution, and Interpolation.
  • Verification witnesses.
Literatura
  • PELED, Doron A. Software reliability methods. New York: Springer, 2001, xix, 331. ISBN 0387951067. info
  • CLARKE, E. M., Orna GRUMBERG, Doron PELED, Daniel KROENING a Helmut VEITH. Model checking. Second edition. Cambridge, Massachusetts: MIT Press, 2018, xx, 402. ISBN 9780262038836. info
  • Handbook of model checking. Edited by E. M. Clarke - T. A. Henzinger - Helmut Veith - Roderick Bloem. Cham: Springer International Publishing AG, 2018, xxiv, 1210. ISBN 9783319105741. info
Výukové metody
lectures
Metody hodnocení
oral exam
Vyučovací jazyk
Angličtina
Další komentáře
Studijní materiály
Předmět je vyučován každoročně.
Předmět je zařazen také v obdobích jaro 2008, jaro 2009, jaro 2010, jaro 2011, jaro 2012, jaro 2013, jaro 2014, jaro 2015, jaro 2016, jaro 2017, jaro 2018, jaro 2019, jaro 2020, jaro 2021, jaro 2022, jaro 2023, podzim 2024.

IA159 Formal Verification Methods

Fakulta informatiky
jaro 2023
Rozsah
2/0. 2 kr. (plus ukončení). Ukončení: zk.
Vyučující
prof. RNDr. Jan Strejček, Ph.D. (přednášející)
Garance
prof. RNDr. Jan Strejček, Ph.D.
Katedra teorie programování – Fakulta informatiky
Dodavatelské pracoviště: Katedra teorie programování – Fakulta informatiky
Rozvrh
Po 13. 2. až Po 15. 5. Po 16:00–17:50 A318
Předpoklady
IA169 System Verif. and Assurance
Omezení zápisu do předmětu
Předmět je nabízen i studentům mimo mateřské obory.
Mateřské obory/plány
předmět má 49 mateřských oborů, zobrazit
Cíle předmětu
At the end of this course, students should understand and be able to explain principles, advantages, and disadvantages of selected methods from the area of formal verification, namely model checking methods, abstraction, static analysis via abstract interpretation, and shape analysis;
make reasoned decisions about suitability of various methods for verification of specific systems;
Výstupy z učení
At the end of this course, students should understand and be able to explain principles, advantages, and disadvantages of selected methods from the area of formal verification, namely model checking methods, abstraction, static analysis via abstract interpretation, and shape analysis;
make reasoned decisions about suitability of various methods for verification of specific systems;
Osnova
  • Overview of formal verification methods.
  • LTL model checking of finite and infinite-state systems including partial order reduction.
  • Abstraction.
  • Counterexample-guided abstraction refinement (CEGAR).
  • Static analysis, abstract interpretation.
  • Shape analysis.
  • Software verification via automata, symbolic execution, and interpolation.
  • Property-Directed Reachability (PDR/IC3).
Literatura
  • PELED, Doron A. Software reliability methods. New York: Springer, 2001, xix, 331. ISBN 0387951067. info
  • GRUMBERG, Orna, Doron A. PELED a E. M. CLARKE. Model checking. Cambridge: MIT Press, 1999, xiv, 314. ISBN 0262032708. info
Výukové metody
lectures
Metody hodnocení
oral exam
Vyučovací jazyk
Angličtina
Další komentáře
Studijní materiály
Předmět je vyučován každoročně.
Předmět je zařazen také v obdobích jaro 2008, jaro 2009, jaro 2010, jaro 2011, jaro 2012, jaro 2013, jaro 2014, jaro 2015, jaro 2016, jaro 2017, jaro 2018, jaro 2019, jaro 2020, jaro 2021, jaro 2022, podzim 2023, podzim 2024.

IA159 Formal Verification Methods

Fakulta informatiky
jaro 2022
Rozsah
2/0. 2 kr. (plus ukončení). Ukončení: zk.
Vyučující
prof. RNDr. Jan Strejček, Ph.D. (přednášející)
Garance
prof. RNDr. Jan Strejček, Ph.D.
Katedra teorie programování – Fakulta informatiky
Dodavatelské pracoviště: Katedra teorie programování – Fakulta informatiky
Rozvrh
Čt 17. 2. až Čt 12. 5. Čt 12:00–13:50 A318
Předpoklady
IV113 Úvod do validace a verifikace || IA169 System Verif. and Assurance
Omezení zápisu do předmětu
Předmět je nabízen i studentům mimo mateřské obory.
Mateřské obory/plány
předmět má 48 mateřských oborů, zobrazit
Cíle předmětu
At the end of this course, students should understand and be able to explain principles, advantages, and disadvantages of selected methods from the area of formal verification, namely model checking methods, abstraction, static analysis via abstract interpretation, and shape analysis;
make reasoned decisions about suitability of various methods for verification of specific systems;
Výstupy z učení
At the end of this course, students should understand and be able to explain principles, advantages, and disadvantages of selected methods from the area of formal verification, namely model checking methods, abstraction, static analysis via abstract interpretation, and shape analysis;
make reasoned decisions about suitability of various methods for verification of specific systems;
Osnova
  • Overview of formal verification methods.
  • LTL model checking of finite and infinite-state systems including partial order reduction.
  • Abstraction.
  • Counterexample-guided abstraction refinement (CEGAR).
  • Static analysis, abstract interpretation.
  • Shape analysis.
  • Software verification via automata, symbolic execution, and interpolation.
  • Property-Directed Reachability (PDR/IC3).
Literatura
  • PELED, Doron A. Software reliability methods. New York: Springer, 2001, xix, 331. ISBN 0387951067. info
  • GRUMBERG, Orna, Doron A. PELED a E. M. CLARKE. Model checking. Cambridge: MIT Press, 1999, xiv, 314. ISBN 0262032708. info
Výukové metody
lectures
Metody hodnocení
oral exam
Vyučovací jazyk
Angličtina
Další komentáře
Studijní materiály
Předmět je vyučován každoročně.
Předmět je zařazen také v obdobích jaro 2008, jaro 2009, jaro 2010, jaro 2011, jaro 2012, jaro 2013, jaro 2014, jaro 2015, jaro 2016, jaro 2017, jaro 2018, jaro 2019, jaro 2020, jaro 2021, jaro 2023, podzim 2023, podzim 2024.

IA159 Formal Verification Methods

Fakulta informatiky
jaro 2021
Rozsah
2/0. 2 kr. (plus ukončení). Ukončení: zk.
Vyučující
prof. RNDr. Jan Strejček, Ph.D. (přednášející)
Garance
prof. RNDr. Jan Strejček, Ph.D.
Katedra teorie programování – Fakulta informatiky
Dodavatelské pracoviště: Katedra teorie programování – Fakulta informatiky
Rozvrh
Po 10:00–11:50 Virtuální místnost
Předpoklady
IV113 Úvod do validace a verifikace || IA169 System Verif. and Assurance
Omezení zápisu do předmětu
Předmět je nabízen i studentům mimo mateřské obory.
Mateřské obory/plány
předmět má 48 mateřských oborů, zobrazit
Cíle předmětu
At the end of this course, students should understand and be able to explain principles, advantages, and disadvantages of selected methods from the area of formal verification, namely model checking methods, abstraction, static analysis via abstract interpretation, and shape analysis;
make reasoned decisions about suitability of various methods for verification of specific systems;
Výstupy z učení
At the end of this course, students should understand and be able to explain principles, advantages, and disadvantages of selected methods from the area of formal verification, namely model checking methods, abstraction, static analysis via abstract interpretation, and shape analysis;
make reasoned decisions about suitability of various methods for verification of specific systems;
Osnova
  • Overview of formal verification methods.
  • LTL model checking of finite and infinite-state systems including partial order reduction.
  • Abstraction.
  • Counterexample-guided abstraction refinement (CEGAR).
  • Static analysis, abstract interpretation.
  • Shape analysis.
  • Software verification via automata, symbolic execution, and interpolation.
  • Property-Directed Reachability (PDR/IC3).
Literatura
  • PELED, Doron A. Software reliability methods. New York: Springer, 2001, xix, 331. ISBN 0387951067. info
  • GRUMBERG, Orna, Doron A. PELED a E. M. CLARKE. Model checking. Cambridge: MIT Press, 1999, xiv, 314. ISBN 0262032708. info
Výukové metody
lectures
Metody hodnocení
oral exam
Vyučovací jazyk
Angličtina
Další komentáře
Studijní materiály
Předmět je vyučován každoročně.
Předmět je zařazen také v obdobích jaro 2008, jaro 2009, jaro 2010, jaro 2011, jaro 2012, jaro 2013, jaro 2014, jaro 2015, jaro 2016, jaro 2017, jaro 2018, jaro 2019, jaro 2020, jaro 2022, jaro 2023, podzim 2023, podzim 2024.

IA159 Formal Verification Methods

Fakulta informatiky
jaro 2020
Rozsah
2/0. 2 kr. (plus ukončení). Ukončení: zk.
Vyučující
prof. RNDr. Jan Strejček, Ph.D. (přednášející)
Garance
prof. RNDr. Jan Strejček, Ph.D.
Katedra teorie programování – Fakulta informatiky
Dodavatelské pracoviště: Katedra teorie programování – Fakulta informatiky
Rozvrh
Po 10:00–11:50 A319
Předpoklady
IV113 Úvod do validace a verifikace || IA169 System Verif. and Assurance
Omezení zápisu do předmětu
Předmět je nabízen i studentům mimo mateřské obory.
Mateřské obory/plány
předmět má 48 mateřských oborů, zobrazit
Cíle předmětu
At the end of this course, students should understand and be able to explain principles, advantages, and disadvantages of selected methods from the area of formal verification, namely model checking methods, abstraction, static analysis via abstract interpretation, and shape analysis;
make reasoned decisions about suitability of various methods for verification of specific systems;
Výstupy z učení
At the end of this course, students should understand and be able to explain principles, advantages, and disadvantages of selected methods from the area of formal verification, namely model checking methods, abstraction, static analysis via abstract interpretation, and shape analysis;
make reasoned decisions about suitability of various methods for verification of specific systems;
Osnova
  • Overview of formal verification methods.
  • LTL model checking of finite and infinite-state systems including partial order reduction.
  • Abstraction.
  • Counterexample-guided abstraction refinement (CEGAR).
  • Static analysis, abstract interpretation.
  • Shape analysis.
  • Software verification via automata, symbolic execution, and interpolation.
  • Property-Directed Reachability (PDR/IC3).
Literatura
  • PELED, Doron A. Software reliability methods. New York: Springer, 2001, xix, 331. ISBN 0387951067. info
  • GRUMBERG, Orna, Doron A. PELED a E. M. CLARKE. Model checking. Cambridge: MIT Press, 1999, xiv, 314. ISBN 0262032708. info
Výukové metody
lectures
Metody hodnocení
oral exam
Vyučovací jazyk
Angličtina
Další komentáře
Studijní materiály
Předmět je vyučován každoročně.
Předmět je zařazen také v obdobích jaro 2008, jaro 2009, jaro 2010, jaro 2011, jaro 2012, jaro 2013, jaro 2014, jaro 2015, jaro 2016, jaro 2017, jaro 2018, jaro 2019, jaro 2021, jaro 2022, jaro 2023, podzim 2023, podzim 2024.

IA159 Formal Verification Methods

Fakulta informatiky
jaro 2019
Rozsah
2/0. 2 kr. (plus ukončení). Ukončení: zk.
Vyučující
prof. RNDr. Jan Strejček, Ph.D. (přednášející)
Garance
prof. RNDr. Mojmír Křetínský, CSc.
Katedra teorie programování – Fakulta informatiky
Dodavatelské pracoviště: Katedra teorie programování – Fakulta informatiky
Rozvrh
St 10:00–11:50 A319
Předpoklady
IV113 Úvod do validace a verifikace || IA169 System Verif. and Assurance
Omezení zápisu do předmětu
Předmět je nabízen i studentům mimo mateřské obory.
Mateřské obory/plány
předmět má 19 mateřských oborů, zobrazit
Cíle předmětu
At the end of this course, students should understand and be able to explain principles, advantages, and disadvantages of selected methods from the area of formal verification, namely model checking methods, abstraction, static analysis via abstract interpretation, and shape analysis;
make reasoned decisions about suitability of various methods for verification of specific systems;
Výstupy z učení
At the end of this course, students should understand and be able to explain principles, advantages, and disadvantages of selected methods from the area of formal verification, namely model checking methods, abstraction, static analysis via abstract interpretation, and shape analysis;
make reasoned decisions about suitability of various methods for verification of specific systems;
Osnova
  • Overview of formal verification methods.
  • LTL model checking of finite and infinite-state systems including translation of LTL to Büchi automata and partial order reduction.
  • Abstraction.
  • Counterexample-guided abstraction refinement.
  • Static analysis, abstract interpretation.
  • Shape analysis.
  • Software verification via automata, symbolic execution, and interpolation.
Literatura
  • PELED, Doron A. Software reliability methods. New York: Springer, 2001, xix, 331. ISBN 0387951067. info
  • GRUMBERG, Orna, Doron A. PELED a E. M. CLARKE. Model checking. Cambridge: MIT Press, 1999, xiv, 314. ISBN 0262032708. info
Výukové metody
lectures
Metody hodnocení
oral exam
Vyučovací jazyk
Angličtina
Další komentáře
Studijní materiály
Předmět je vyučován každoročně.
Předmět je zařazen také v obdobích jaro 2008, jaro 2009, jaro 2010, jaro 2011, jaro 2012, jaro 2013, jaro 2014, jaro 2015, jaro 2016, jaro 2017, jaro 2018, jaro 2020, jaro 2021, jaro 2022, jaro 2023, podzim 2023, podzim 2024.

IA159 Formal Verification Methods

Fakulta informatiky
jaro 2018
Rozsah
2/0. 2 kr. (plus ukončení). Ukončení: zk.
Vyučující
prof. RNDr. Jan Strejček, Ph.D. (přednášející)
Garance
prof. RNDr. Mojmír Křetínský, CSc.
Katedra teorie programování – Fakulta informatiky
Dodavatelské pracoviště: Katedra teorie programování – Fakulta informatiky
Rozvrh
Čt 12:00–13:50 B410
Předpoklady
IV113 Úvod do validace a verifikace || IA169 System Verif. and Assurance
Omezení zápisu do předmětu
Předmět je nabízen i studentům mimo mateřské obory.
Mateřské obory/plány
předmět má 19 mateřských oborů, zobrazit
Cíle předmětu
At the end of this course, students should understand and be able to explain principles, advantages, and disadvantages of selected methods from the area of formal verification, namely model checking methods, abstraction, static analysis via abstract interpretation, and shape analysis;
make reasoned decisions about suitability of various methods for verification of specific systems;
Výstupy z učení
At the end of this course, students should understand and be able to explain principles, advantages, and disadvantages of selected methods from the area of formal verification, namely model checking methods, abstraction, static analysis via abstract interpretation, and shape analysis;
make reasoned decisions about suitability of various methods for verification of specific systems;
Osnova
  • Overview of formal verification methods.
  • LTL model checking of finite and infinite-state systems including translation of LTL to Büchi automata and partial order reduction.
  • Abstraction.
  • Counterexample-guided abstraction refinement.
  • Static analysis, abstract interpretation.
  • Shape analysis.
  • Software verification via automata, symbolic execution, and interpolation.
Literatura
  • PELED, Doron A. Software reliability methods. New York: Springer, 2001, xix, 331. ISBN 0387951067. info
  • GRUMBERG, Orna, Doron A. PELED a E. M. CLARKE. Model checking. Cambridge: MIT Press, 1999, xiv, 314. ISBN 0262032708. info
Výukové metody
lectures
Metody hodnocení
oral exam
Vyučovací jazyk
Angličtina
Další komentáře
Studijní materiály
Předmět je vyučován každoročně.
Předmět je zařazen také v obdobích jaro 2008, jaro 2009, jaro 2010, jaro 2011, jaro 2012, jaro 2013, jaro 2014, jaro 2015, jaro 2016, jaro 2017, jaro 2019, jaro 2020, jaro 2021, jaro 2022, jaro 2023, podzim 2023, podzim 2024.

IA159 Formal Verification Methods

Fakulta informatiky
jaro 2017
Rozsah
2/0. 2 kr. (plus ukončení). Ukončení: zk.
Vyučující
prof. RNDr. Jan Strejček, Ph.D. (přednášející)
Garance
prof. RNDr. Mojmír Křetínský, CSc.
Katedra teorie programování – Fakulta informatiky
Dodavatelské pracoviště: Katedra teorie programování – Fakulta informatiky
Rozvrh
St 10:00–11:50 A319
Předpoklady
IV113 Úvod do validace a verifikace || IA169 System Verif. and Assurance
Omezení zápisu do předmětu
Předmět je nabízen i studentům mimo mateřské obory.
Mateřské obory/plány
předmět má 19 mateřských oborů, zobrazit
Cíle předmětu
At the end of this course, students should understand and be able to explain principles, advantages, and disadvantages of selected from the area of formal verification, namely model checking methods, abstraction, static analysis via abstract interpretation, and shape analysis;
make reasoned decisions about suitability of various methods for verification of specific systems;
Osnova
  • Overview of formal verification methods.
  • LTL model checking of finite and infinite-state systems including translation of LTL to Büchi automata and partial order reduction.
  • Abstraction.
  • Counter-example guided abstraction refinement.
  • Static analysis, abstract interpretation.
  • Shape analysis.
  • Software verification via automata, symbolic execution, and interpolation.
Literatura
  • PELED, Doron A. Software reliability methods. New York: Springer, 2001, xix, 331. ISBN 0387951067. info
  • GRUMBERG, Orna, Doron A. PELED a E. M. CLARKE. Model checking. Cambridge: MIT Press, 1999, xiv, 314. ISBN 0262032708. info
Výukové metody
lectures
Metody hodnocení
oral exam
Vyučovací jazyk
Angličtina
Další komentáře
Studijní materiály
Předmět je vyučován každoročně.
Předmět je zařazen také v obdobích jaro 2008, jaro 2009, jaro 2010, jaro 2011, jaro 2012, jaro 2013, jaro 2014, jaro 2015, jaro 2016, jaro 2018, jaro 2019, jaro 2020, jaro 2021, jaro 2022, jaro 2023, podzim 2023, podzim 2024.

IA159 Formal Verification Methods

Fakulta informatiky
jaro 2016
Rozsah
2/0. 2 kr. (plus ukončení). Ukončení: zk.
Vyučující
prof. RNDr. Jan Strejček, Ph.D. (přednášející)
Garance
prof. RNDr. Mojmír Křetínský, CSc.
Katedra teorie programování – Fakulta informatiky
Dodavatelské pracoviště: Katedra teorie programování – Fakulta informatiky
Rozvrh
St 12:00–13:50 A318
Předpoklady
IV113 Úvod do validace a verifikace || IA169 System Verif. and Assurance
Omezení zápisu do předmětu
Předmět je nabízen i studentům mimo mateřské obory.
Mateřské obory/plány
předmět má 19 mateřských oborů, zobrazit
Cíle předmětu
At the end of this course, students should understand and be able to explain principles, advantages, and disadvantages of selected from the area of formal verification, namely model checking methods, abstraction, static analysis via abstract interpretation, and shape analysis;
make reasoned decisions about suitability of various methods for verification of specific systems;
Osnova
  • Overview of formal verification methods.
  • LTL model checking of finite and infinite-state systems including translation of LTL to Büchi automata and partial order reduction.
  • Abstraction.
  • Counter-example guided abstraction refinement.
  • Static analysis, abstract interpretation.
  • Shape analysis.
  • Software verification via automata, symbolic execution, and interpolation.
Literatura
  • PELED, Doron A. Software reliability methods. New York: Springer, 2001, xix, 331. ISBN 0387951067. info
  • GRUMBERG, Orna, Doron A. PELED a E. M. CLARKE. Model checking. Cambridge: MIT Press, 1999, xiv, 314. ISBN 0262032708. info
Výukové metody
lectures
Metody hodnocení
oral exam
Vyučovací jazyk
Angličtina
Další komentáře
Studijní materiály
Předmět je vyučován každoročně.
Předmět je zařazen také v obdobích jaro 2008, jaro 2009, jaro 2010, jaro 2011, jaro 2012, jaro 2013, jaro 2014, jaro 2015, jaro 2017, jaro 2018, jaro 2019, jaro 2020, jaro 2021, jaro 2022, jaro 2023, podzim 2023, podzim 2024.

IA159 Formal Verification Methods

Fakulta informatiky
jaro 2015
Rozsah
2/0. 2 kr. (plus ukončení). Ukončení: zk.
Vyučující
prof. RNDr. Jan Strejček, Ph.D. (přednášející)
Garance
prof. RNDr. Mojmír Křetínský, CSc.
Katedra teorie programování – Fakulta informatiky
Dodavatelské pracoviště: Katedra teorie programování – Fakulta informatiky
Rozvrh
Čt 12:00–13:50 B410
Předpoklady
IA006 Automaty
It is recommended to attend courses IA040 Modální a temporální logiky procesů and IV113 Úvod do validace a verifikace before registering this course.
Omezení zápisu do předmětu
Předmět je nabízen i studentům mimo mateřské obory.
Mateřské obory/plány
předmět má 18 mateřských oborů, zobrazit
Cíle předmětu
At the end of this course, students should be able to: understand and explain principles, advantages, and disadvantages of basic formal verification methods, namely model checking methods, symbolic execution, abstract interpretation, and theorem proving;
make reasoned decisions about suitability of various methods for verification of specific systems;
Osnova
  • Overview of formal verification methods.
  • Deductive verification methods (theorem proving).
  • LTL model checking of finite and infinite-state systems.
  • Abstraction.
  • Counter-example guided abstraction refinement.
  • Bounded model checking.
  • Symbolic execution.
  • Static analysis, abstract interpretation.
  • Verification tools.
Literatura
  • PELED, Doron A. Software reliability methods. New York: Springer, 2001, xix, 331. ISBN 0387951067. info
  • GRUMBERG, Orna, Doron A. PELED a E. M. CLARKE. Model checking. Cambridge: MIT Press, 1999, xiv, 314. ISBN 0262032708. info
Výukové metody
lectures
Metody hodnocení
oral exam
Vyučovací jazyk
Angličtina
Další komentáře
Studijní materiály
Předmět je vyučován každoročně.
Předmět je zařazen také v obdobích jaro 2008, jaro 2009, jaro 2010, jaro 2011, jaro 2012, jaro 2013, jaro 2014, jaro 2016, jaro 2017, jaro 2018, jaro 2019, jaro 2020, jaro 2021, jaro 2022, jaro 2023, podzim 2023, podzim 2024.

IA159 Formal Verification Methods

Fakulta informatiky
jaro 2014
Rozsah
2/0. 2 kr. (plus ukončení). Ukončení: zk.
Vyučující
prof. RNDr. Jan Strejček, Ph.D. (přednášející)
Garance
prof. RNDr. Mojmír Křetínský, CSc.
Katedra teorie programování – Fakulta informatiky
Dodavatelské pracoviště: Katedra teorie programování – Fakulta informatiky
Rozvrh
Čt 14:00–15:50 B411
Předpoklady
IA006 Automaty
It is recommended to attend courses IA040 Modální a temporální logiky procesů and IV113 Úvod do validace a verifikace before registering this course.
Omezení zápisu do předmětu
Předmět je nabízen i studentům mimo mateřské obory.
Mateřské obory/plány
předmět má 18 mateřských oborů, zobrazit
Cíle předmětu
At the end of this course, students should be able to: understand and explain principles, advandtages, and disadvantages of basic formal verification methods, namely model checking methods, symbolic execution, abstract interpretation, and theorem proving;
make reasoned decisions about suitability of various methods for verification of specific systems;
Osnova
  • Overview of formal verification methods.
  • Deductive verification methods (theorem proving).
  • LTL model checking of finite and infinite-state systems.
  • State explosion problem, partial order reduction, abstraction.
  • Counter-example guided abstraction refinement.
  • Bounded model checking.
  • Symbolic execution.
  • Static analysis, abstract interpretation.
  • Verification tools.
Literatura
  • PELED, Doron A. Software reliability methods. New York: Springer, 2001, xix, 331. ISBN 0387951067. info
  • GRUMBERG, Orna, Doron A. PELED a E. M. CLARKE. Model checking. Cambridge: MIT Press, 1999, xiv, 314. ISBN 0262032708. info
  • Model-Based Testing, http://www.goldpractices.com/practices/mbt/
Výukové metody
lectures
Metody hodnocení
oral exam
Vyučovací jazyk
Angličtina
Další komentáře
Studijní materiály
Předmět je vyučován každoročně.
Předmět je zařazen také v obdobích jaro 2008, jaro 2009, jaro 2010, jaro 2011, jaro 2012, jaro 2013, jaro 2015, jaro 2016, jaro 2017, jaro 2018, jaro 2019, jaro 2020, jaro 2021, jaro 2022, jaro 2023, podzim 2023, podzim 2024.

IA159 Formal Verification Methods

Fakulta informatiky
jaro 2013
Rozsah
2/0. 2 kr. (plus ukončení). Ukončení: zk.
Vyučující
doc. Mgr. Jan Obdržálek, PhD. (přednášející)
Garance
prof. RNDr. Mojmír Křetínský, CSc.
Katedra teorie programování – Fakulta informatiky
Kontaktní osoba: doc. Mgr. Jan Obdržálek, PhD.
Dodavatelské pracoviště: Katedra teorie programování – Fakulta informatiky
Rozvrh
Po 12:00–13:50 G123
Předpoklady
IA006 Automaty
It is recommended to attend courses IA040 Modální a temporální logiky procesů and IV113 Úvod do validace a verifikace before registering this course.
Omezení zápisu do předmětu
Předmět je nabízen i studentům mimo mateřské obory.
Mateřské obory/plány
předmět má 18 mateřských oborů, zobrazit
Cíle předmětu
At the end of this course, students should be able to: understand and explain principles of basic formal verification methods, namely model checking methods, reachability analysis, symbolic execution, abstract interpretations, and theorem proving;
make reasoned decisions about suitability of various methods for verification of specific systems;
Osnova
  • Overview of formal verification methods.
  • Software testing.
  • Deductive verification methods (theorem proving).
  • LTL model checking of finite and infinite-state systems.
  • State explosion problem, partial order reduction, abstraction.
  • Counter-example guided abstraction refinement.
  • Symbolic execution.
  • Static analysis, abstract interpretation.
  • Verification tools.
Literatura
  • PELED, Doron A. Software reliability methods. New York: Springer, 2001, xix, 331. ISBN 0387951067. info
  • GRUMBERG, Orna, Doron A. PELED a E. M. CLARKE. Model checking. Cambridge: MIT Press, 1999, xiv, 314. ISBN 0262032708. info
  • Model-Based Testing, http://www.goldpractices.com/practices/mbt/
Výukové metody
lectures
Metody hodnocení
oral exam
Vyučovací jazyk
Angličtina
Další komentáře
Studijní materiály
Předmět je vyučován každoročně.
Předmět je zařazen také v obdobích jaro 2008, jaro 2009, jaro 2010, jaro 2011, jaro 2012, jaro 2014, jaro 2015, jaro 2016, jaro 2017, jaro 2018, jaro 2019, jaro 2020, jaro 2021, jaro 2022, jaro 2023, podzim 2023, podzim 2024.

IA159 Formal Verification Methods

Fakulta informatiky
jaro 2012
Rozsah
2/0. 2 kr. (plus ukončení). Ukončení: zk.
Vyučující
prof. RNDr. Jan Strejček, Ph.D. (přednášející)
doc. Mgr. Jan Obdržálek, PhD. (pomocník)
Garance
prof. RNDr. Mojmír Křetínský, CSc.
Katedra teorie programování – Fakulta informatiky
Kontaktní osoba: prof. RNDr. Jan Strejček, Ph.D.
Dodavatelské pracoviště: Katedra teorie programování – Fakulta informatiky
Rozvrh
Út 14:00–15:50 B204
Předpoklady
IA006 Automaty
It is recommended to attend courses IA040 Modální a temporální logiky procesů and IV113 Úvod do validace a verifikace before registering this course.
Omezení zápisu do předmětu
Předmět je nabízen i studentům mimo mateřské obory.
Mateřské obory/plány
předmět má 22 mateřských oborů, zobrazit
Cíle předmětu
At the end of this course, students should be able to: understand and explain principles of basic formal verification methods, namely model checking methods, reachability analysis, symbolic execution, abstract interpretations, and theorem proving;
make reasoned decisions about suitability of various methods for verification of specific systems;
Osnova
  • Overview of formal verification methods.
  • Software testing.
  • Deductive verification methods (theorem proving).
  • LTL model checking of finite and infinite-state systems.
  • State explosion problem, partial order reduction, abstraction.
  • Counter-example guided abstraction refinement.
  • Symbolic execution.
  • Static analysis, abstract interpretation.
  • Verification tools.
Literatura
  • PELED, Doron A. Software reliability methods. New York: Springer, 2001, xix, 331. ISBN 0387951067. info
  • GRUMBERG, Orna, Doron A. PELED a E. M. CLARKE. Model checking. Cambridge: MIT Press, 1999, xiv, 314. ISBN 0262032708. info
  • Model-Based Testing, http://www.goldpractices.com/practices/mbt/
Výukové metody
lectures
Metody hodnocení
oral exam
Vyučovací jazyk
Angličtina
Další komentáře
Studijní materiály
Předmět je vyučován každoročně.
Předmět je zařazen také v obdobích jaro 2008, jaro 2009, jaro 2010, jaro 2011, jaro 2013, jaro 2014, jaro 2015, jaro 2016, jaro 2017, jaro 2018, jaro 2019, jaro 2020, jaro 2021, jaro 2022, jaro 2023, podzim 2023, podzim 2024.

IA159 Formal Verification Methods

Fakulta informatiky
jaro 2011
Rozsah
2/0. 2 kr. (plus ukončení). Ukončení: zk.
Vyučující
prof. RNDr. Jan Strejček, Ph.D. (přednášející)
Garance
prof. RNDr. Mojmír Křetínský, CSc.
Katedra teorie programování – Fakulta informatiky
Kontaktní osoba: prof. RNDr. Jan Strejček, Ph.D.
Rozvrh
Út 8:00–9:50 A107
Předpoklady
IA006 Automaty
It is recommended to attend courses IA040 and IV113 before registering this course.
Omezení zápisu do předmětu
Předmět je nabízen i studentům mimo mateřské obory.
Mateřské obory/plány
předmět má 21 mateřských oborů, zobrazit
Cíle předmětu
At the end of this course, students should be able to: understand and explain principles of basic formal verification methods, namely model checking methods, reachability analysis, abstract interpretations, and theorem proving;
make reasoned decisions about suitability of various methods for verification of specific systems;
Osnova
  • Overview of formal verification methods.
  • Software testing.
  • Deductive verification methods (theorem proving).
  • LTL model checking of finite and infinite-state systems.
  • State explosion problem, partial order reduction, abstraction.
  • Counter-example guided abstraction refinement.
  • Static analysis, abstract interpretation.
  • Verification tools.
Literatura
  • PELED, Doron A. Software reliability methods. New York: Springer, 2001, xix, 331. ISBN 0387951067. info
  • GRUMBERG, Orna, Doron A. PELED a E. M. CLARKE. Model checking. Cambridge: MIT Press, 1999, xiv, 314. ISBN 0262032708. info
  • Model-Based Testing, http://www.goldpractices.com/practices/mbt/
Výukové metody
lectures
Metody hodnocení
oral exam
Vyučovací jazyk
Angličtina
Další komentáře
Studijní materiály
Předmět je vyučován každoročně.
Předmět je zařazen také v obdobích jaro 2008, jaro 2009, jaro 2010, jaro 2012, jaro 2013, jaro 2014, jaro 2015, jaro 2016, jaro 2017, jaro 2018, jaro 2019, jaro 2020, jaro 2021, jaro 2022, jaro 2023, podzim 2023, podzim 2024.

IA159 Formal Verification Methods

Fakulta informatiky
jaro 2010
Rozsah
2/0. 2 kr. (plus ukončení). Ukončení: zk.
Vyučující
prof. RNDr. Jan Strejček, Ph.D. (přednášející)
Garance
prof. RNDr. Mojmír Křetínský, CSc.
Katedra teorie programování – Fakulta informatiky
Kontaktní osoba: prof. RNDr. Jan Strejček, Ph.D.
Rozvrh
Čt 16:00–17:50 B411
Předpoklady
IA006 Automaty
It is recommended to attend courses IA040 and IV113 before registering this course.
Omezení zápisu do předmětu
Předmět je nabízen i studentům mimo mateřské obory.
Mateřské obory/plány
předmět má 21 mateřských oborů, zobrazit
Cíle předmětu
At the end of this course, students should be able to: understand and explain principles of basic formal verification methods, namely model checking methods, reachability analysis, abstract interpretations, and theorem proving;
make reasoned decisions about suitability of various methods for verification of specific systems;
Osnova
  • Overview of formal verification methods.
  • Software testing.
  • Deductive verification methods (theorem proving).
  • LTL model checking of finite and infinite-state systems.
  • State explosion problem, partial order reduction, abstraction.
  • Counter-example guided abstraction refinement.
  • Static analysis, abstract interpretation.
  • Verification tools.
Literatura
  • PELED, Doron A. Software reliability methods. New York: Springer, 2001, xix, 331. ISBN 0387951067. info
  • GRUMBERG, Orna, Doron A. PELED a E. M. CLARKE. Model checking. Cambridge: MIT Press, 1999, xiv, 314. ISBN 0262032708. info
  • Model-Based Testing, http://www.goldpractices.com/practices/mbt/
Výukové metody
lectures
Metody hodnocení
oral exam
Vyučovací jazyk
Angličtina
Další komentáře
Studijní materiály
Předmět je vyučován každoročně.
Předmět je zařazen také v obdobích jaro 2008, jaro 2009, jaro 2011, jaro 2012, jaro 2013, jaro 2014, jaro 2015, jaro 2016, jaro 2017, jaro 2018, jaro 2019, jaro 2020, jaro 2021, jaro 2022, jaro 2023, podzim 2023, podzim 2024.

IA159 Formal Verification Methods

Fakulta informatiky
jaro 2009
Rozsah
2/0. 2 kr. (plus ukončení). Ukončení: zk.
Vyučující
prof. RNDr. Jan Strejček, Ph.D. (přednášející)
Garance
prof. RNDr. Mojmír Křetínský, CSc.
Katedra teorie programování – Fakulta informatiky
Kontaktní osoba: prof. RNDr. Jan Strejček, Ph.D.
Rozvrh
Čt 12:00–13:50 B411
Předpoklady
IA006 Automaty
It is recommended to attend courses IA040 and IV113 before registering this course.
Omezení zápisu do předmětu
Předmět je nabízen i studentům mimo mateřské obory.
Mateřské obory/plány
předmět má 18 mateřských oborů, zobrazit
Cíle předmětu
Formal verification aims to verify correctness or improve reliability of software and hardware systems. At the end of this course, students should understand and be able to explain principles of basic formal verification methods (model checking methods, reachability analysis, abstract interpretations, and theorem proving). Students should also understand advantages and disadvantages of the metioned methods and techniques. Some crucial techniques (abstraction, partial order reduction, etc.) will be discussed in detail.
Osnova
  • Models of systems
  • Formal specification of program properties (modal and temporal logics)
  • Automatic verification - reachability analysis, symbolic and explicit model checking, equivalence checking
  • Deductive verification methods (theorem proving)
  • Software testing
  • Program analysis, abstraction, abstract interpretation
  • Counter-example guided abstraction refinement
  • Combining formal methods, SW tools BLAST, Spec# etc.
Literatura
  • PELED, Doron A. Software reliability methods. New York: Springer, 2001, xix, 331. ISBN 0387951067. info
  • GRUMBERG, Orna, Doron A. PELED a E. M. CLARKE. Model checking. Cambridge: MIT Press, 1999, xiv, 314. ISBN 0262032708. info
  • Model-Based Testing, http://www.goldpractices.com/practices/mbt/
Metody hodnocení
lectures, oral exam
Vyučovací jazyk
Angličtina
Další komentáře
Studijní materiály
Předmět je vyučován každoročně.
Předmět je zařazen také v obdobích jaro 2008, jaro 2010, jaro 2011, jaro 2012, jaro 2013, jaro 2014, jaro 2015, jaro 2016, jaro 2017, jaro 2018, jaro 2019, jaro 2020, jaro 2021, jaro 2022, jaro 2023, podzim 2023, podzim 2024.

IA159 Formal Verification Methods

Fakulta informatiky
jaro 2008
Rozsah
2/0. 2 kr. (plus ukončení). Ukončení: zk.
Vyučující
prof. RNDr. Jan Strejček, Ph.D. (přednášející)
Garance
prof. RNDr. Mojmír Křetínský, CSc.
Katedra teorie programování – Fakulta informatiky
Kontaktní osoba: prof. RNDr. Jan Strejček, Ph.D.
Rozvrh
Čt 10:00–11:50 B411
Předpoklady
IA006 Automaty
It is recommended to attend courses IA040 and IV113 before registering this course.
Omezení zápisu do předmětu
Předmět je nabízen i studentům mimo mateřské obory.
Mateřské obory/plány
předmět má 18 mateřských oborů, zobrazit
Cíle předmětu
Formal verification aims to verify correctness or improve reliability of software and hardware systems. The course introduces current methods of formal verification (model checking methods, reachability analysis, abstract interpretations, and theorem proving), from theoretical principles to practical tools. The course also mentions basic specification and modeling formalisms, specific aspects of hardware and software verification, position of formal verification in system development process, etc.
Osnova
  • Models of systems
  • Formal specification of program properties (modal and temporal logics)
  • Automatic verification - reachability analysis, symbolic and explicit model checking, equivalence checking
  • Deductive verification methods (theorem proving)
  • Software testing
  • Program analysis, abstraction, abstract interpretation
  • Counter-example guided abstraction refinement
  • Combining formal methods, SW tools BLAST, Spec# etc.
Literatura
  • PELED, Doron A. Software reliability methods. New York: Springer, 2001, xix, 331. ISBN 0387951067. info
  • GRUMBERG, Orna, Doron A. PELED a E. M. CLARKE. Model checking. Cambridge: MIT Press, 1999, xiv, 314. ISBN 0262032708. info
  • Model-Based Testing, http://www.goldpractices.com/practices/mbt/
  • David Schmidt: Abstract interpretation and static analysis, http://www.cis.ksu.edu/santos/schmidt/Escuela03/home.html
Vyučovací jazyk
Angličtina
Informace učitele
There will be an oral exam at the end of the course.
Další komentáře
Předmět je vyučován každoročně.
Předmět je zařazen také v obdobích jaro 2009, jaro 2010, jaro 2011, jaro 2012, jaro 2013, jaro 2014, jaro 2015, jaro 2016, jaro 2017, jaro 2018, jaro 2019, jaro 2020, jaro 2021, jaro 2022, jaro 2023, podzim 2023, podzim 2024.

IA159 Formal Verification Methods

Fakulta informatiky
jaro 2007

Předmět se v období jaro 2007 nevypisuje.

Rozsah
2/0. 2 kr. (plus ukončení). Ukončení: zk.
Vyučující
prof. RNDr. Jan Strejček, Ph.D. (přednášející)
Garance
prof. RNDr. Mojmír Křetínský, CSc.
Katedra teorie programování – Fakulta informatiky
Kontaktní osoba: prof. RNDr. Jan Strejček, Ph.D.
Předpoklady
It is recommended to complete courses IA006, IA040, and IV113 before registering this course.
Omezení zápisu do předmětu
Předmět je nabízen i studentům mimo mateřské obory.
Mateřské obory/plány
předmět má 6 mateřských oborů, zobrazit
Cíle předmětu
Formal verification aims to verify correctness or improve reliability of software and hardware systems. The course introduces current methods of formal verification (model checking methods, reachability analysis, abstract interpretations, and theorem proving), from theoretical principles to practical tools. The course also mentions basic specification and modeling formalisms, specific aspects of hardware and software verification, position of formal verification in system development process, etc.
Osnova
  • Models of systems
  • Formal specification of program properties (modal and temporal logics)
  • Automatic verification - reachability analysis, symbolic and explicit model checking, equivalence checking
  • Deductive verification methods (theorem proving)
  • Software testing
  • Program analysis, abstraction, abstract interpretation
  • Counter-example guided abstraction refinement
  • Combining formal methods, SW tools BLAST, SPEC etc.
Literatura
  • PELED, Doron A. Software reliability methods. New York: Springer, 2001, xix, 331. ISBN 0387951067. info
  • GRUMBERG, Orna, Doron A. PELED a E. M. CLARKE. Model checking. Cambridge: MIT Press, 1999, xiv, 314. ISBN 0262032708. info
  • Model-Based Testing, http://www.goldpractices.com/practices/mbt/
  • David Schmidt: Abstract interpretation and static analysis, http://www.cis.ksu.edu/santos/schmidt/Escuela03/
Vyučovací jazyk
Angličtina
Další komentáře
Předmět je vyučován každoročně.
Výuka probíhá každý týden.
Předmět je zařazen také v obdobích jaro 2008, jaro 2009, jaro 2010, jaro 2011, jaro 2012, jaro 2013, jaro 2014, jaro 2015, jaro 2016, jaro 2017, jaro 2018, jaro 2019, jaro 2020, jaro 2021, jaro 2022, jaro 2023, podzim 2023, podzim 2024.