The Australian National
      University
College of Engineering and Computer Science
School of Computer Science
Printer Friendly Version of this
    Document
High Performance Scientific Computing COMP2600

COMP2600: Formal Methods for Software Engineering

Lecture Material and Schedule

Lectures slides and associated material will be posted here as the semester progresses.

All being well, lecture recordings will be available through the COMP2600 Wattle site.

  • Revision: Propositional Logic, Predicate Calculus
    Week 1, Monday
    Slides: [pdf] [pdf 2×2]
  • Revision: Sets, Functions, Relations, Induction
    Week 1, Thursday
    Slides: [pdf] [pdf 2×2]
  • No Lecture (Bush Week)
    Week 1, Friday
  • Revision: Basic Haskell
    Week 2, Monday
    Slides: [pdf] [pdf 2×2]
  • Natural Deduction
    Week 2, Wednesday
    Slides: [pdf] [pdf 2×2] [Propositional Calculus Rules]
  • Natural Deduction (continued)
    Week 2, Friday
    Slides: [pdf] [pdf 2×2] [Predicate Calculus Rules]
  • Soundness, Completeness and Consistency
    Week 3, Monday
    Slides: [pdf] [pdf 2×2]
  • Types and Recursion
    Week 3, Thursday
    Slides: [pdf] [pdf 2×2]
    Example code: [Expression.hs]
  • Structural Induction
    Week 3, Friday
    Slides: [pdf] [pdf 2×2]
  • Structural Induction (continued)
    Week 4, Monday
    Slides: [pdf] [pdf 2×2]
  • Hoare Logic
    Week 4, Thursday & Friday; Week 5, Monday
    Slides: [pdf] [pdf 2×2]
  • Weakest Preconditions
    Week 5, Thursday & Friday; Week 6, Monday
    Slides: [pdf] [pdf 2×2]
  • Lambda Calculus
    Week 6, Thursday
    Slides: [pdf] [pdf 2×2]
    [Lambda Calculus Workbench]
    [Mt. Lambda, near Kyoto U.]
  • Church Encoding
    Week 6, Friday
    Slides: [pdf] [pdf 2×2]
  • In-Class Practice Quiz
    Week 7, Monday
    During this class students may attempt a practice quiz to help gauge their progress. It is not for credit. The quiz will cover all material up to and including weakest preconditions. Ideally, you should come prepared with an A4 page of hand-written notes (both sides), as will be permitted in the final exam. The test should take about 1 hour to complete.
  • Type Checking
    Week 7, Thursday
    (Back to the lambda calculus...)
    Slides: [pdf] [pdf 2×2]
  • Finite State Automata & Regular Languages
    Week 7, Friday; continuing later
    Slides: [pdf] [pdf 2×2]
  • Practice Quiz Discussion
    Week 8, Monday
    In this lecture we will work through some of the practice quiz questions. If you did not manage to complete the quiz during class, you should do so in your own time before this class.
    Here is Clem's attempt at the practice quiz.
  • No Lecture
    Week 8, Thursday
  • Finite State Automata & Regular Languages
    Week 8, Friday; Week 9, Monday
    Slides: [continued from week 7 - see above.]
  • Language and Grammars
    Week 9, Thursday
    Slides: [pdf] [pdf 2×2]
  • Push-Down Automata
    Week 9, Friday
    Slides: [pdf] [pdf 2×2]
  • Introduction to Parsing
    Week 10, Monday
    Slides: [pdf] [pdf 2×2]
    Example code: [ParseTypeDefs.hs] [Expression Evaluator]
  • Turing Machines
    Week 10, Thursday
    Slides: [pdf] [pdf 2×2]
  • Complexity and Computability
    Week 10, Friday
    Slides: [pdf] [pdf 2×2]
  • Course Review
    Week 12, Thursday and Friday
    [2008 Exam Paper] [ 2×1]