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

Tuesday lectures: 2pm-4pm, Quadrangle G045 (K-E15-G045).

Wednesday lectures: 12pm-1pm, Quadrangle G027 (K-E15-G027).

Week Dates Content Slides/Notes Lecturer
1 04/03
05/03
Introduction
Automata
Lecture 1
Lecture 2
Franck, Peter
2 11/03
12/03
Temporal Logics
Expressiveness and Fairness
Lecture 3
Lecture 4
Franck
Peter
3 18/03
19/03
LTL Büchi Automata (1)
LTL Büchi Automata (2)
Lecture 5
Lecture 6
Peter
4 25/03
26/03
CTL Model Checking
Summary and Exercises
Lecture 7
Lecture 8
Franck
5 01/04
02/04
Symbolic CTL Model Checking -- 1
Binary Decision Diagrams
Lecture 9
Lecture 10
Franck
6 08/04
09/04
Symbolic Model Checking -- 2
Tools -- 1: CBMC
Lecture 11
Lecture 12
Franck
7 15/04

16/04
Tools -- 2: SPIN

nuSMV, Assignment 1 - Solution
Lecture 13
Examples SPIN
Lecture 14
Peter
Mid-semester break (19 April to 27 April)
8 29/04
30/04
Abstraction Refinement (1)
Abstraction Refinement (2)
Lecture 14
Lecture 15
Franck
9 06/05
07/05
Static Analysis
Source code analysis tool: Goanna
Lecture 16
Lecture 17
Franck
10 13/05
14/05
Timed Automata
Reachability in Timed Automata
Lecture 18
Lecture 19
Franck
11 20/05
21/05
Assignment 2
Model Checking for Timed Automata
Lecture 20
Lecture 21
Peter
12 27/05
28/05
Real-time model checker: UPPAAL
Assignment 3,
Closing remarks, Internships, ToR, Theses at NICTA
Lecture 22
Lecture 23
Advertising
Peter
Franck
13 03/06
04/06
Summary, Questions and Answers
Assignment 4, Questions and Answers
Summary Franck


Copyright 2014 UNSW