SubjectsSubjects(version: 945)
Course, academic year 2023/2024
   Login via CAS
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
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.
Class: Informatika Mgr. - volitelný
Classification: Informatics > Software Engineering
Is incompatible with: NSWX132
Is interchangeable with: NSWX132
Annotation -
Last update: Tajemník Katedry (22.04.2013)
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).
Literature -
Last update: 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

Syllabus -
Last update: Tajemník Katedry (29.04.2014)

Model checking of programs

Detecting concurrency errors

Symbolic execution

Dynamic analysis

Introduction to deductive methods

  • SAT solvers, SMT solvers

Bounded model checking

Predicate abstraction and CEGAR

Selected applications of deductive methods in software verification

  • Verification of program code against contracts

Static analysis and its usage in program verification

Abstract interpretation

Combination of verification techniques

Program termination

Program synthesis

 
Charles University | Information system of Charles University | http://www.cuni.cz/UKEN-329.html