**The Basics**

The first part of the course covers semantics and the encodig of transition functions.

- *Introduction and motivation: *Outline of the course, the necessity for automated verification (software desasters), success stories, and potention future applications

- *One small step for a man: *Small step semantics: Hoare logic and Dijkstra's predicate transformers, Kripke structures, encoding transition functions.

**Part I**

From single step transitions to bounded model checking, specifying reachability and temporal logic properties, and the computation of fixed points.

- *Bounded Model Checking: *Specifying and checking reachability/safety properties, unwinding transition functions, completeness conditions (reachability/recurrence diameter). Shows how BMC can be applied to check safety properties for software ("local" rather than "monolitic" transition functions). Discusses application for automated test-case generation.

- *Decision Procedures: * How do we decide the instances of formulas generated by BMC? Satisfiability (SAT) checking, Satisfiability-Modulo-Theory (SMT) solvers, Binary Decision Diagrams (BDDs)

-* Approximating Fixed Points (Craig Interpolation): *Approximating Fixed Points with Craig Interpolation

-* Partial* *Order Reduction (optional): *Reducing the size of the state-space for concurrent models by means of partial order reduction (POR)

**Part II: To infinity and beyond**

Shows how the ideas presented in part I can be applied to infinite state systems (and actual software programs rather than models) by means of *abstraction.* Introduces static analysis using abstract interpretation, predicate abstraction, and interpolation-based software model checking. The course may cover advanced concepts such as rely/guarantee reasoning for parallel programs (Owicki-Gries) and temination proving, if time permits.

- *the Concept of Abstraction (Abstract Interpretation): *Static analysis of programs using abstraction and abstract domains. Disjunctive domains and loss of precision.

- * Predicate Abstraction and Automated Refinement: *Tracking facts about program states using first-order logic predicates.Automatically refining abstractions using Counterexample-Guided Abstraction-Refinement (CEGAR)

- *Lazy Abstraction, Interpolation-based Software Model Checking: *Contemporary techniques for predicate abstraction and automated refinement

- *Concurrent Software *Hoare logic for parallel programs with shared memory. Owicki-Gries, Cliff Jones' rely-guarantee reasoning (compositional reasoning). Automatic refinement of environment assumptions. Global vs. local invariants and *ghost * variables. Also addresses incomplete approaches such as context-bounded model checking.

This course is taught in English and held online.

Zoom Meetings Tuesday:

Meeting ID: 954 1816 7847

Password: SoMoCh20

https://tuwien.zoom.us/j/95418167847?pwd=eTZ1aEE4R3dOQ2Z5VFZIaU9xem1mdz09

Zoom Meetings Friday:

Meeting ID: 983 6354 2656

Password: SoMoCh20

https://tuwien.zoom.us/j/98363542656?pwd=VDRKZEk3enZzTlVCNkxNYUJ4eWh0Zz09