Course Program (draft)

Introduction. Introduction to formal methods, formal guarantees, review of propositional and first-order logic, model checking/querying and reasoning (satisfiability, validity, and logical implication). Tableaux for propositional and first-order logic.

Abstract operational semantics and partial correctness. Abstract operational semantics for programs: evaluation semantics (whole computation) and transition semantics (single step of the computation). Hoare Logics, weakest precondition, invariants of programs. Partial correctness, total correctness.

Transition system and fixpoints. Reactive/interactive programs (finite state), transition systems, reachability, bisimulation. Fixpoints, Knaster-Tarski theorem on least and greatest fixpoint, approximates for least and greatest fixpoint.

Verification of dynamic systems. Verification of dynamic and temporal properties on transition systems: Safeness, Liveness, Fairness, Strong Fairness. Temporal logic for verification: LTL, CTL, CTL*, mu-calculus. Model checking for mu-calculus. Model checking for CTL via translation to mu-calculus. Model checking for LTL via automata. LTL satisfiability via Tableaux

Focusing on finite traces. Regular Automata, Linear Temporal Logics on finite traces, LTLf, LDLf, Pure Past LTL, connections to automata, computing DFAs, Manipulating DFAs, Reasoning on finite traces. LTLf Tableaux.

Reactive synthesis. Automated program synthesis, synthesis from specifications in Linear Temporal Logic on finite traces, game-theoretic view, arena and objective, adversarial reachability.