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.