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.