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 2020
• Semestr: letní
• E-Kredity: 5
• Rozsah, examinace: letní s.:2/2, Z+Zk [HT]
• Počet míst: neomezen
• Minimální obsazenost: neomezen
• 4EU+: ne
• Virtuální mobilita / počet míst pro virtuální mobilitu: ne
• 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: doc. RNDr. Pavel Parízek, Ph.D.
• Vyučující: doc. RNDr. Pavel Parízek, Ph.D.
• Třída: Informatika Mgr. - volitelný
• Kategorizace předmětu: Informatika > Softwarové inženýrství
• Je neslučitelnost pro: NSWX132
• Je záměnnost pro: NSWX132

Anotace

čeština

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

Poslední úprava: Katedry Tajemník (22.04.2013)

angličtina

Basic principles of automated analysis and verification of programs (model checking, static analysis, dynamic analysis, and deductive methods) and their practical applications (e.g., detecting concurrency errors).

Poslední úprava: Katedry Tajemník (22.04.2013)

Literatura

čeština

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

Poslední úprava: T_KSI (23.02.2009)

Sylabus

čeština

Model checking programů

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

Symbolické vykonávání

Dynamická analýza

Fuzz testování

Ú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

• pokročilé aspekty 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ů

Poslední úprava: Parízek Pavel, doc. RNDr., Ph.D. (14.05.2024)

angličtina

Model checking of programs

Detecting concurrency errors

Symbolic execution

Dynamic analysis

Fuzz testing

Introduction to deductive methods

• SAT solvers, SMT solvers

Bounded model checking

Predicate abstraction and CEGAR

Selected applications of deductive methods in software verification

• Advanced topics in verification of program code against contracts

Static analysis and its usage in program verification

Abstract interpretation

Combination of verification techniques

Program termination

Program synthesis

Poslední úprava: Parízek Pavel, doc. RNDr., Ph.D. (14.05.2024)