Decision Procedures for Verification

Slides

  • 24.10.2016: Introduction [introduction.pdf]
  • 31.10.2016: Propositional logic (1) [prop-logic1.pdf]
  • 7.11.2016: Propositional logic (2) [prop-logic2.pdf]
  • 14.11.2016: Propositional logic (3) [prop-logic3.pdf]
  • 21.11.2016: Propositional logic (4), First-order logic (1) [prop-logic4.pdf]
  • 28.11.2016: First-order logic (2) [first-order-logic2.pdf]
  • 5.12.2016: First-order logic (3) [first-order-logic3.pdf]
  • 12.12.2016: First-order logic (4) + Decision Procedures (1) [first-order-logic4.pdf]
  • 09.01.2017: Decision procedures (2) [decproc-2.pdf]
  • 12.01.2017: Decision procedures (3) [decproc-3.pdf]
  • Example (congruence closure) [congruence-closure-example.pdf]
  • 16.01.2017: Decision procedures (4) [decproc-4.pdf]
  • Examples (difference logic) [difference-logic-examples.pdf]
  • Examples (difference logic with < and <=) [difference-logic-examples2.pdf]
  • 23.01.2017: Decision procedures (5) [decproc-5.pdf]
  • Examples (Fourier-Motzkin) example 1, example 2
  • Examples (Loos-Weispfenning) example 1, example 2
  • 30.1.2017: Combinations of decision procedures (1) [combinations1.pdf]
  • 2.2.2017: Combinations of decision procedures (2) [combinations2.pdf]
  • 6.2.2017: Combinations of decision procedures (3) [combinations3.pdf]
  • 13.2.2017: Combinations of decision procedures (4); Applications [combinations4.pdf]