Formal Specification and Verification


Folien

  • 16.04.2013: Motivation [intro.pdf]
  • 18.04.2013: Classical logic 1 [logic-1.pdf]
  • 23.04.2013: Classical logic 2 [logic-2.pdf]
  • 30.04.2013: Classical logic 3 (BDD, OBDD) [logic-3.pdf]
  • 2.05.2013: Classical logic 4 (OBDD, First-order logic) [logic-4.pdf]
  • 14.05.2013: Classical logic 5 (First-order logic; Formal Specification (generalities); Algebraic specification 1) [logic-5.pdf]
  • 14.05.2013: Algebraic specification (Slides by Bidoit and Mosses) (will be discussed also in the lecture on 16.05.2013)
  • 16.05.2013: Algebraic specification 2, Transition systems [trans-systems.pdf]
  • 4.06.2013: Transition systems and generalizations [trans-systems2.pdf]
  • 6.06.2013: Generalizations of transition systems: Timed automata and hybrid automata [trans-systems3.pdf]
  • 6.06.2013: Other specification languages + example [specification-others.pdf]
  • 6.06.2013: Temporal logic 1: Introduction [temporal-logic1.pdf]
  • 18.06.2013: Temporal logic 2: LTL [temporal-logic2.pdf] (last change: 24.07.2013, page 16)
  • 20.06.2013: Temporal logic 3: LTL,CTL [temporal-logic3.pdf]
  • 25.06.2013: Temporal logic 4: Model Checking [temporal-logic4.pdf] (Updated: 28.06.2013)
  • 02.07.2013: Temporal logic 5: Model Checking with OBDD [temporal-logic5.pdf] (last change: 24.07.2013, page 25)
  • 02.07.2013: Dynamic Logic 1: Introduction [dynamic-logic1.pdf]
  • 04.07.2013: Dynamic Logic 2: Syntax, Semantics, Axiom system [dynamic-logic2.pdf] (last change: 24.07.2013, page 10)
  • 09.07.2013: Dynamic Logic 3: PDL -- Soundness, Completeness, Decidability [dynamic-logic3.pdf]
  • Soundness, completeness and decidability proof for PDL [decidability-pdl.pdf]
  • 09.07.2013: Deductive Verification 1 [deductive-verification1.pdf]
  • 16.07.2013: Deductive Verification 2 [deductive-verification2.pdf] (last change: 24.07.2013, page 32)