Formal Specification and Verification
Folien
25.10.2016: Motivation
[introduction.pdf]
27.10.2016: Classical logic 1
[logic-1.pdf]
08.11.2016: Classical logic 2
[logic-2.pdf]
10.11.2016: Classical logic 3
[logic-3.pdf]
15.11.2016: Classical logic 4
[logic-4.pdf]
The examples discussed on the blackboard can be found on pages 372-382 of the book ``Logic in Computer Science'' by Huth and Ryan.
22.11.2016: Classical logic 5 (First-order logic)
[logic-5.pdf]
24.11.2016: Theories, Algebraic specification (generalities)
[logic-6.pdf]
(Changed on 1 December 2016: Added slides on Herbrand interpretations (p.9-11))
29.11.2016:
Algebraic Specification (we discussed a subset of the slides below)
(Slides by Bidoit and Mosses)
Systems for satisfiability checking in propositional and first-order logic;
Systems for reasoning about algebraic specifications
The materials are included in the following .zip file:
[materials-provers.zip]
Transition systems (introduction)
[trans-systems1.pdf]
6.12.2016: Transition systems, ASM, Timed automata, Hybrid automata
[trans-systems2.pdf]
13.12.2016: Hybrid automata (ctd.); CSP; more expressive languages (example)
[trans-systems3.pdf]
13.12.2016: Temporal logic 1: Introduction
[temporal-logic1.pdf]
10.01.2017: Temporal logic 2: LTL
[temporal-logic2.pdf]
12.01.2017: Temporal logic 3: LTL ctd.; CTL
[temporal-logic3.pdf]
17.01.2017: Temporal logic 4: CTL ctd.; Model Checking 1
[temporal-logic4.pdf]
Example 1:
[.pdf]
24.01.2017: Temporal logic 5: Model Checking 2
[temporal-logic5.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
31.01.2017: Dynamic Logic 1
[dynamic-logic-1.pdf]
7.02.2017: Dynamic Logic 2: PDL - Soundness, Completeness, Decidability; Sequent calculus
[dynamic-logic-2.pdf]
Soundness, completeness and decidability proof for PDL
[decidability-pdl.pdf]
7.02.2017: Deductive Verification 1
[deductive-verification1.pdf]
14.02.2017: Deductive Verification 2
[deductive-verification2.pdf]
Example: iteration of post:
[pdf]