Decision Procedures for Verification

Slides

  • 21.10.2013: Introduction [introduction.pdf]
  • 21.10.2013: Propositional logic (1) [prop-logic1.pdf]
  • 31.10.2013: Propositional logic (2) [prop-logic2.pdf]
  • 5.11.2013: Propositional logic (3); First-order logic (1) [prop-logic3.pdf]
  • 14.11.2013: First-order logic (2) [first-order-logic2.pdf]
  • 21.11.2013: First-order logic (3) [first-order-logic3.pdf]
  • 28.12.2013: First-order logic (4) + Decision Procedures (1) [first-order-logic4.pdf] (4.12.13: added x as argument on pages 27 and 28)
  • 5.12.2013: Decision procedures (1) [decproc-1.pdf]
  • 12.12.2013: Decision procedures (2) [decproc-2.pdf]
  • Example (congruence closure) [congruence-closure-example.pdf]
  • Examples (difference logic) [difference-logic-examples.pdf]
  • 19.12.2013: Decision procedures (3) [decproc-3.pdf]
  • Examples (difference logic with < and <=) [difference-logic-examples2.pdf]
  • Examples (Fourier-Motzkin) example 1, example 2
  • Examples (Loos-Weispfenning) example 1, example 2
  • 9.1.2014: Decision Procedures (4) + Combinations of decision procedures (1) [combinations1.pdf]
  • 16.1.2014: Combinations of decision procedures (2) [combinations2.pdf]
  • 23.1.2014: Combinations of decision procedures (3) [combinations3.pdf]
  • 30.1.2014: Combinations of decision procedures (4) [combinations4.pdf]
  • 06.02.2014: Applications [applications.pdf]