The course covers several fundamental techniques for the analysis  of programs, with focus on safety and security. The techniques are based on modeling concurrent systems, types and logics for programs, and allow to discover certain types of illicit behaviour or deduce the absence of such behaviour. We consider several successful tools implementing such techniques

Course contents:

• Introduction to Safety and Security.
• Part 1: Model checking: System modeling, temporal logics, liveness and safety, model checking, tools.
• Part 2: Concurrency, non-determinism in software: Multi-threading, concurrency analysis, testing and verifying concurrency, analysis of networked software.
• Part 3: Information security: Information flow analysis, security architecture, access control, type systems, analysis of information flow.
• Part 4: Risk and threat analysis, forensics, security testing. Risk and threat modeling, safety and security standards, forensics, fuzz testing, memory safety checking.

The preliminary schedule for the course includes of 11 lectures and 5 labs.

The course is given in English.