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