Formal Verification and Specification

Folien

  • 17.04.2012: Motivation [intro.pdf]
  • 24.04.2012: Classical Logic (Part 1: Propositional logic: Syntax,Semantics,CNF,Hilbert Calculus) [classical-logic1.pdf]
  • 8.05.2012: Classical Logic (Part 2: Propositional logic: Sequent calculus, Resolution, DPLL, BDD) [classical-logic2.pdf]
  • 10.05.2012: Classical Logic (Part 3: OBDDs) [classical-logic3.pdf]
  • 15.05.2012: First-Order Logic (Part 1) [first-order-logic1.pdf]
  • Additional slides: Algorithmic Problems/Undecidability/Decidability [dec-undec-fol.pdf]
  • 22.05.2012: Logical Theories; Formal Specification (generalities); Algebraic specification [first-order-logic2-adt.pdf]
  • 22.05.2012: Algebraic specification (Slides by Bidoit and Mosses) [.pdf]
  • 05.06.2012: Transition systems and generalizations [trans-systems.pdf]
  • 12.06.2012: Specification (An example) [specification-3.pdf]
  • 12.06.2012: Temporal logic [temporal-logic.pdf]
  • 19.06.2012: Temporal logic, Part 2 [temporal-logic-2.pdf]
  • 26.06.2012: Temporal logic, Part 3 [temporal-logic-mc-obdd.pdf]
  • Proof 1
  • Example Model Checking
  • Example Model Checking with OBDDs
  • 3.07.2012: Propositional dynamic logic [pdl.pdf]
  • Soundness, completeness and decidability proof for PDL [decidability-pdl.pdf] (draft)
  • 10.07.2012: Deductive verification (an introduction) [deductive-verification.pdf]