Decision Procedures for Verification

Slides

  • 24.10.2022

  • 27.11.2022: Propositional logic (2) [prop-logic2.pdf]

  • 31.10.2022 Propositional logic (3) [prop-logic3.pdf]

  • 7.11.2022 Propositional logic (4) [prop-logic4.pdf]

  • 14.11.2022: First-order logic (1) [first-order-logic1.pdf]

  • 21.11.2022: First-order logic (2) [first-order-logic2.pdf]

  • 28.11.2022: First-order logic (3) [first-order-logic3.pdf] (after the lecture)

  • 5.12.2022: First-order logic (4) [first-order-logic4.pdf]

  • 12.12.2022:
  • First-order logic (5) [first-order-logic5.pdf]
  • Decision procedures (1) [decproc1.pdf]
  • 19.12.2022: Decision procedures (2) [decproc2.pdf]
  • 22.12.2022: Decision procedures (3) [decproc3.pdf]
  • Example (congruence closure) [congruence-closure-example.pdf]
  • The same example with more details [congruence-closure-example.pdf]

  • Examples (difference logic) [difference-logic-examples.pdf] (discussed partially on 22.12; to be discussed further on 09.01.23)

  • Audio Commented Slides (Online: 21.2.2022)

    •
  • 09.01.2023: Decision procedures (4) [decproc4.pdf]
  • Examples (difference logic) [difference-logic-examples.pdf] (discussed partially on 22.12; to be discussed further on 09.01.23)

  • Examples (difference logic with < and <=) [difference-logic-examples2.pdf]
  • Example (Fourier-Motzkin) example 1 , example 2
  • Examples (Loos-Weispfenning) example 1, example 2

  • Audio Commented Slides (Online: 9.1.2023)

    •
  • 16.01.2023 Combinations of decision procedures (1) [combinations1.pdf]
  • Using the Nelson-Oppen procedure - Guessing variant [nelson-oppen-examples-guessing.pdf]
  • Using the Nelson-Oppen procedure - Backtracking variant [nelson-oppen-examples-backtracking.pdf]

  • Audio Commented Slides (Online: 22.1.2023)

    •
  • 23.01.2023: Combinations of decision procedures (2) [combinations2.pdf]
  • Audio Commented Slides (Online: 23.1.2023)

    •
  • 30.01.2023: Combinations of decision procedures (3); DPLL(T); Instantiation; Applications [combinations3.pdf]

  • 6.02.2022: Overview - Topics for the exam [summary.pdf]
    • Additional Material
  • The Calculus of Computation: slides calculus-of-computation-slides.pdf