Subjects

Your browser does not support JavaScript, or its support is disabled. Some features may not be available.

Program Analysis and Code Verification - NSWI132

Title:	Analýza programů a verifikace kódu
Guaranteed by:	Department of Distributed and Dependable Systems (32-KDSS)
Faculty:	Faculty of Mathematics and Physics
Actual:	from 2020
Semester:	summer
E-Credits:	5
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
Additional information:	http://d3s.mff.cuni.cz/teaching/nswi132
Note:	enabled for web enrollment

Guarantor:	doc. RNDr. Pavel Parízek, Ph.D.
Teacher(s):	doc. RNDr. Pavel Parízek, Ph.D.
Class:	Informatika Mgr. - volitelný
Classification:	Informatics > Software Engineering
Is incompatible with:	NSWX132
Is interchangeable with:	NSWX132

Opinion survey results Examination dates SS schedule Noticeboard

Annotation -

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)

Literature -

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 -

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)