Analýza programů a verifikace kódu

Sylabus

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ů

Anotace

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).