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 (2008–2010): Missionaries and Cannibals

  This exercise requires the use of the SMV tool, which in version 2.4.3 does not compile on some machines because of the code’s use of the reserved function name malloc.  Please apply this patch to fix this problem.

• Assessable Exercise (2011): Colour Rotation Puzzle

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.

Other Material

• Lecture given to COMP 2600 (in 2010 and 2011) about the L4.verified project.