Course Program

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. 

Analysis and verification of static aspects. Syntax and semantics of class-based conceptual diagrams such as UML Class Diagrams and Entity Relationship Diagrams. Verification of static properties. Use of first-order logic for automated reasoning on such diagrams. Chase for full dependencies for completing UML Class Diagrams instances. 

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. 

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