Formal Specification and Verification

22.10.2018: Motivation [introduction.pdf]

23.10.2018: Classical logic 1 [logic-1.pdf] (after the lecture)

30.10.2018: Classical logic 2 [logic-2.pdf] (after the lecture)

5.11.2018: Classical logic 3 [logic-3.pdf] (after the lecture)

6.11.2018 and 12.11.2018: Classical logic 4 [logic-4.pdf] (after the lecture on 12.11.18)

The examples discussed on the blackboard can be found on pages 372-382 of the book ``Logic in Computer Science'' by Huth and Ryan. [pages 372-382]

13.11.2018: Classical logic 5 [logic-5.pdf]

19.11.2018: Theories, Algebraic specification (generalities) [logic-6.pdf]

Algebraic Specification (we discussed a subset of the slides below)
(Slides by Bidoit and Mosses)
Further informations can be found on the CoFi CASL website, under CASL Tools
and on the Hets website and on the Hets web-based interface

26.11.2018: Transition systems (1) [trans-systems1.pdf]

3.12.2018: Transition systems, ASM, Timed automata, Hybrid automata [trans-systems2.pdf]

10.12.2018 and 11.12.2018: Temporal logic 1 [temporal-logic1.pdf] 21.02.2019: Typo corrected on page 38 (the formula was correct in Exercise 8.1)

17.12.2018: Temporal logic 2 [temporal-logic2.pdf]

7.01.2019: Temporal logic 3: CTL ctd.; model checking [temporal-logic3.pdf]

Example 1: [.pdf]

14.01.2019: Temporal logic 4: Model Checking 2 [temporal-logic4.pdf]

Example 1 new solution: [.pdf]
Example 2: [.pdf]
Examples: Modeling with OBDDs: [.pdf]
Examples (using NuSMV)
- README.txt (How to use NuSMV)
- example2.txt
- ferryman.txt

21.01.2019, 22.01.2019 and 28.01.2019: Dynamic Logic 1 [dynamic-logic-1.pdf] 21.02.2019: Correction on slides 56 and 58

Soundness, completeness and decidability proof for PDL [decidability-pdl.pdf]

28.01.2019: Deductive Verification 1 [deductive-verification1.pdf]

Example: iteration of post: [pdf]

4.02.2019: Deductive Verification 2 [deductive-verification2.pdf] 21.02.2019: Typo on slide 15 corrected - as discussed in the Q&A Session