Formal Specification and Verification

Folien

  • 22.04.2014: Motivation [introduction.pdf]
  • 24.04.2014: Classical logic 1 [logic-1.pdf] (last update: 29.04.14, 20:00)
  • 29.04.2014: Classical logic 2 [logic-2.pdf] (last update: 29.04.14, 20:00)
  • 6.05.2014: Classical logic 3 [logic-3.pdf]
  • 13.05.2014: Classical logic 4 (First-order logic; Formal Specification (generalities); Algebraic specification 1) [logic-4.pdf]
  • 13.05.2014: Algebraic specification (Slides by Bidoit and Mosses)
  • 20.05.2014: (Matthias Horbach)
  • 27.05.2014: Transition systems, ASM, Timed automata [trans-systems.pdf]
  • 3.06.2014: Generalizations of transition systems: Timed automata and hybrid automata; CSP; more expressive languages [trans-systems2.pdf]
  • 3.06.2014: Temporal logic 1: Introduction [temporal-logic1.pdf]
  • 17.06.2014: Temporal logic 2: LTL [temporal-logic2.pdf]
  • 24.06.2014: Temporal logic 3: LTL ctd. [temporal-logic3.pdf]
  • 1.07.2014: Temporal logic 4: CTL ctd. [temporal-logic4.pdf]
  • 3.07.2014: Temporal logic 5: Model Checking 1 [temporal-logic5.pdf] (last change: 8.07.2014, page 8)
  • 08.07.2014: Temporal logic 6: Model Checking with OBDD [temporal-logic6.pdf]
  • 15.07.2014: Dynamic Logic 1 [dynamic-logic-1.pdf]
  • 22.07.2014: Dynamic Logic 2: PDL - Soundness, Completeness, Decidability; Sequent calculus [dynamic-logic-2.pdf]
  • Soundness, completeness and decidability proof for PDL [decidability-pdl.pdf]
  • 24.07.2014: Deductive Verification 1 [deductive-verification1.pdf]
  • 29.07.2014: Deductive Verification 2 [deductive-verification2.pdf]
  • Example: iteration of post: [pdf]