PředmětyPředměty(verze: 837)
Předmět, akademický rok 2018/2019
   Přihlásit přes CAS
Analýza programů a verifikace kódu - NSWI132
Anglický název: Program Analysis and Code Verification
Zajišťuje: Katedra distribuovaných a spolehlivých systémů (32-KDSS)
Fakulta: Matematicko-fyzikální fakulta
Platnost: od 2015
Semestr: letní
E-Kredity: 6
Rozsah, examinace: letní s.:2/2 Z+Zk [hodiny/týden]
Počet míst: neomezen
Minimální obsazenost: neomezen
Stav předmětu: vyučován
Jazyk výuky: angličtina
Způsob výuky: prezenční
Další informace: http://d3s.mff.cuni.cz/teaching/nswi132
Poznámka: povolen pro zápis po webu
Garant: RNDr. Pavel Parízek, Ph.D.
Třída: Informatika Mgr. - volitelný
Kategorizace předmětu: Informatika > Softwarové inženýrství
Anotace -
Poslední úprava: Tajemník Katedry (22.04.2013)
Základní principy automatické analýzy a verifikace programů (model checking, statická analýza, dynamická analýza, a deduktivní metody) a jejich praktická aplikace (například hledání chyb ve vícevláknových programech).
Literatura -
Poslední úprava: T_KSI (23.02.2009)

E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking, MIT Press, 2000

F. Nielson, H. R. Nielson, and Chris Hankin. Principles of Program Analysis, Springer, 2005

D. Kroening and O. Strichman. Decision Procedures: An Algorithmic Point of View, Springer, 2008

Sylabus -
Poslední úprava: Tajemník Katedry (29.04.2014)

Model checking programů

Hledání chyb ve vícevláknových programech

Symbolické vykonávání

Dynamická analýza

Úvod do deduktivních metod

  • SAT solvers, SMT solvers

Omezený model checking

Predikátová abstrakce a CEGAR

Vybrané aplikace deduktivních metod ve verifikaci software

  • verifikace programů proti kontraktům

Statická analýza kódu a její použití ve verifikaci programů

Abstraktní interpretace

Kombinace technik verifikace

Terminace programů

Syntéza programů

 
Univerzita Karlova | Informační systém UK