This time table is tentative, and may be subject to change.

Tuesday lectures: 2pm-4pm, Ainsworth Building 201 (K-J17-201).

Thursday lectures: 1pm-2pm, The Michael Hintze Theatre (K-H6-LG03)

Week Dates Contents (tbc) Slides/Notes References
1 01/03
03/03
Introduction
Automata
Lecture 1
Lecture 2
Huth/Ryan $1, Sipser $1.1-1.2
Bayer/Katoen $2.1-2.2 (Parts)
2 08/03
10/03
Temporal Logics
Expressiveness
Lecture 3
Lecture 4
Huth/Ryan $3.2, $3.4, Bayer/Katoen $5.1,6.2 (Parts)
Huth/Ryan $3.5, Bayer/Katoen $6.3 (Parts)
3 15/03
17/03
CTL Model Checking
LTL and Büchi automata
Lecture 5
Lecture 6
Bérard et al. $3.1, Bayer/Katoen $6.4, Clarke et al. $4.1
Bayer/Katoen $5.2
4 22/03
24/03
 
LTL Model Checking
Tool: Spin
 
Lecture 7
Lecture 8
Spin: Examples
Bayer/Katoen $5.2
http://spinroot.com/;
http://spinroot.com/spin/Man/Quick.html
Mid-semester break (28 March to 1 April)
5 05/04
07/04
Static Analysis
Tool: Goanna
Lecture 9
Lecture 10
Nielsen/Nielsen/Hankin
 
6 12/04
 
14/04
 
Symbolic CTL Model Checking (1)
 
Binary Decision Diagrams
 
Lecture 11
Lect. 11 short
Lecture 12
Lect. 12 short
tba
 
tba
 
7 19/04
 
21/04
Symbolic CTL Model Checking (2)
 
Assignment 1
Lecture 13
Lect. 13 short
 
tba
 
 
8 26/04
28/04
Assignment 1, Tool: CBMC
Assignment 2
Lecture 14
Announcement
CBMC webpage
 
9 03/05
05/05
Abstraction Refinement (1)
Abstraction Refinement (2)
Lecture 15
Lecture 16
Clarke et al. CEGAR (2000)
tba
10 10/05
12/05
Timed Automata
Region Graph
Lecture 17
Lecture 18
tba
tba
11 17/05
19/06
 
Timed Languages
Timed Logics
Assignment 3 (maybe)
Lecture 19
Lecture 20
 
12 24/05
 
26/05
Model Checking for Timed Automata
Assignment 3
Real-time model checker: UPPAAL
Lecture 21
 
Lecture 22
13 31/05
 
Summary, Questions and Answers
(optional)
 


Copyright 2016