• Publications
• Teaching Material

Temporal Logic and Model Checking

These lectures were given as part of an “overview of logic and computation” course in Semester 1 of 2009. Very similar material was presented as part of a similar course in 2008 as well.

• Lecture 1: Modal Logic
• Lecture 2: CTL
• Lecture 3: Explicit State Model Checking
• Lecture 4: BDDs and Symbolic Model Checking
• Lecture 5: Topics in Model Checking (Counter-examples, Bounded Model Checking, Optimisations)
• Lecture 6: LTL Model Checking
• Assessable Exercise

Logic Summer School Material

The ANU and NICTA have combined to present two-week long Logic Summer Schools since 2003.  I have taken part in most (all?) of these.

Automated Reasoning: Arithmetic

Slides on arithmetic decision procedures (from February 2009), covering Fourier-Motzkin variable elimination, the Omega Test and Cooper’s method.

Computability and Incompleteness

From December 2009.

• Lecture 1: Computational Models
• Lecture 2: Computability Results
• Lecture 3: Logic and Computability
• Lecture 4: Gödel’s First Incompleteness Theorem
• Lecture 5: Gödel’s Second Incompleteness Theorem

The course referred to the following books:

• Computability and Logic, George Boolos and Richard Jeffrey. ISBN 0-521-38923-2.
• Gödel’s Theorem: An Incomplete Guide to Its Use and Abuse, Torkel Franzén. ISBN 1-56881-238-8.
• Notes on Logic and Set Theory, P. Johnstone. ISBN 0-521-33692-9.
• Introduction to Mathematical Logic, Elliott Mendelson. ISBN 0-412-80830-7.