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

Modulo Theory).

 

The course will have ~4 exercises and a final project (that can be done in pairs.)
Prerequisite: Computational models (0368-2200)