Program Analysis and Code Verification - NSWX132

• Title: Analýza programů a verifikace kódu
• Guaranteed by: Student Affairs Department (32-STUD)
• Faculty: Faculty of Mathematics and Physics
• Actual: from 2022
• Semester: summer
• E-Credits: 6
• Hours per week, examination: summer s.:2/2, C+Ex [HT]
• Capacity: unlimited
• Min. number of students: unlimited
• 4EU+: no
• Virtual mobility / capacity: no
• State of the course: taught
• Language: English
• Teaching methods: full-time
• Is provided by: NSWI132
• Additional information: http://d3s.mff.cuni.cz/teaching/nswi132
• Note: enabled for web enrollment
• Guarantor: doc. RNDr. Pavel Parízek, Ph.D.
• Class: Informatika Mgr. - volitelný
• Classification: Informatics > Software Engineering
• Pre-requisite : {NXXX010, NXXX026, NXXX034, NXXX035}
• Incompatibility : NSWI132
• Interchangeability : NSWI132

Annotation

English

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

Last update: Katedry Tajemník (22.04.2013)

Czech

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

Last update: Katedry Tajemník (22.04.2013)

Literature

English

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

Last update: T_KSI (23.02.2009)

Syllabus

English

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 synthesis

Last update: Parízek Pavel, doc. RNDr., Ph.D. (16.02.2025)

Czech

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

Syntéza programů

Last update: Parízek Pavel, doc. RNDr., Ph.D. (16.02.2025)