Formal Specification and Verification
Folien
16.04.2013: Motivation
[intro.pdf]
18.04.2013: Classical logic 1
[logic-1.pdf]
23.04.2013: Classical logic 2
[logic-2.pdf]
30.04.2013: Classical logic 3 (BDD, OBDD)
[logic-3.pdf]
2.05.2013: Classical logic 4 (OBDD, First-order logic)
[logic-4.pdf]
14.05.2013: Classical logic 5 (First-order logic; Formal Specification (generalities); Algebraic specification 1)
[logic-5.pdf]
14.05.2013: Algebraic specification
(Slides by Bidoit and Mosses)
(will be discussed also in the lecture on 16.05.2013)
16.05.2013: Algebraic specification 2, Transition systems
[trans-systems.pdf]
4.06.2013: Transition systems and generalizations
[trans-systems2.pdf]
6.06.2013: Generalizations of transition systems: Timed automata and hybrid automata
[trans-systems3.pdf]
6.06.2013: Other specification languages + example
[specification-others.pdf]
6.06.2013: Temporal logic 1: Introduction
[temporal-logic1.pdf]
18.06.2013: Temporal logic 2: LTL
[temporal-logic2.pdf]
(last change: 24.07.2013, page 16)
20.06.2013: Temporal logic 3: LTL,CTL
[temporal-logic3.pdf]
25.06.2013: Temporal logic 4: Model Checking
[temporal-logic4.pdf]
(Updated: 28.06.2013)
Example 1:
[.pdf]
Example 2:
[.pdf]
Modeling with OBDDs:
[.pdf]
02.07.2013: Temporal logic 5: Model Checking with OBDD
[temporal-logic5.pdf]
(last change: 24.07.2013, page 25)
02.07.2013: Dynamic Logic 1: Introduction
[dynamic-logic1.pdf]
04.07.2013: Dynamic Logic 2: Syntax, Semantics, Axiom system
[dynamic-logic2.pdf]
(last change: 24.07.2013, page 10)
09.07.2013: Dynamic Logic 3: PDL -- Soundness, Completeness, Decidability
[dynamic-logic3.pdf]
Soundness, completeness and decidability proof for PDL
[decidability-pdl.pdf]
09.07.2013: Deductive Verification 1
[deductive-verification1.pdf]
16.07.2013: Deductive Verification 2
[deductive-verification2.pdf]
(last change: 24.07.2013, page 32)