SubjectsSubjects(version: 845)
Course, academic year 2018/2019
   Login via CAS
Program Analysis and Code Verification - NSWI132
Title in English: 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 2015 to 2019
Semester: summer
E-Credits: 6
Hours per week, examination: summer s.:2/2 C+Ex [hours/week]
Capacity: unlimited
Min. number of students: unlimited
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: RNDr. Pavel Parízek, Ph.D.
Class: Informatika Mgr. - volitelný
Classification: Informatics > Software Engineering
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