Decision Procedures for Verification

Slides

  • 28.10.2014: Introduction [introduction.pdf]
  • 28.10.2014: Propositional logic (1) [prop-logic1.pdf]
  • 4.11.2014: Propositional logic (2) [prop-logic2.pdf]
  • 11.11.2014: Propositional logic (3) [prop-logic3.pdf]
  • 18.11.2014: Propositional logic (4), First-order logic (1) [prop-logic4.pdf]
  • 25.11.2014: First-order logic (2) [first-order-logic2.pdf] (after the lecture)
  • 2.12.2014: First-order logic (3) [first-order-logic3.pdf] (after the lecture)
  • 9.12.2014: First-order logic (4) [first-order-logic4.pdf] (after the lecture)
  • 16.12.2014: Decision procedures (1) [decproc-1.pdf] (after the lecture)
  • 08.01.2015: Decision procedures (2) [decproc-2.pdf]
  • Example (congruence closure) [congruence-closure-example.pdf]
  • 13.01.2015: Decision procedures (3) [decproc-3.pdf]
  • Examples (difference logic) [difference-logic-examples.pdf]
  • Examples (difference logic with < and <=) [difference-logic-examples2.pdf]
  • Examples (Fourier-Motzkin) example 1, example 2
  • Examples (Loos-Weispfenning) example 1, example 2
  • 20.1.2015: Decision Procedures (4) + Combinations of decision procedures (1) [combinations1.pdf]
  • 27.1.2015: Combinations of decision procedures (2) [combinations2.pdf]
  • 3.2.2015: Combinations of decision procedures (3) [combinations3.pdf]
  • 10.2.2015: Combinations of decision procedures (4) [combinations4.pdf]