Formal Specification and Verification


Folien

  • 25.10.2016: Motivation [introduction.pdf]
  • 27.10.2016: Classical logic 1 [logic-1.pdf]
  • 08.11.2016: Classical logic 2 [logic-2.pdf]
  • 10.11.2016: Classical logic 3 [logic-3.pdf]
  • 15.11.2016: Classical logic 4 [logic-4.pdf]
  • The examples discussed on the blackboard can be found on pages 372-382 of the book ``Logic in Computer Science'' by Huth and Ryan.
  • 22.11.2016: Classical logic 5 (First-order logic) [logic-5.pdf]

  • 24.11.2016: Theories, Algebraic specification (generalities) [logic-6.pdf]
    (Changed on 1 December 2016: Added slides on Herbrand interpretations (p.9-11))

  • 29.11.2016:
  • 6.12.2016: Transition systems, ASM, Timed automata, Hybrid automata [trans-systems2.pdf]
  • 13.12.2016: Hybrid automata (ctd.); CSP; more expressive languages (example) [trans-systems3.pdf]
  • 13.12.2016: Temporal logic 1: Introduction [temporal-logic1.pdf]
  • 10.01.2017: Temporal logic 2: LTL [temporal-logic2.pdf]
  • 12.01.2017: Temporal logic 3: LTL ctd.; CTL [temporal-logic3.pdf]
  • 17.01.2017: Temporal logic 4: CTL ctd.; Model Checking 1 [temporal-logic4.pdf]
  • Example 1: [.pdf]
  • 24.01.2017: Temporal logic 5: Model Checking 2 [temporal-logic5.pdf]
  • 31.01.2017: Dynamic Logic 1 [dynamic-logic-1.pdf]
  • 7.02.2017: Dynamic Logic 2: PDL - Soundness, Completeness, Decidability; Sequent calculus [dynamic-logic-2.pdf]
  • Soundness, completeness and decidability proof for PDL [decidability-pdl.pdf]
  • 7.02.2017: Deductive Verification 1 [deductive-verification1.pdf]
  • 14.02.2017: Deductive Verification 2 [deductive-verification2.pdf]
  • Example: iteration of post: [pdf]