Operational semantics (How do we formally define the meaning of programs).
Program logics (Classical and modern approaches for manual verification of computer programs).
Abstract interpretation (Theoretical foundation of automatic compile-time
analysis, aka static analysis, For example, determining during compile time whether x= y / z is always 1 or that at this program point z is not zero.)
Miscellaneous verification techniques: MC (Model
checking), SAT (Satisfiability) and SMT (Satisfiability
The course will have ~4 exercises and a final project (that can be done in pairs.)
Prerequisite: Computational models (0368-2200)