Course Outline

Staff

Lecturer: June Andronick
Email: june.andronick at nicta.com.au
Phone: +61 2 8306 0581 Office: Level 6, Building L5
Consultations: by appointment

Lecturer: Gerwin Klein
Email: gerwin.klein at nicta.com.au
Phone: +61 2 8306 0578
Office: E615, Level 6, Building L5
Consultations: by appointment

Course Goal

To give a broader overview of formal modelling and proof techniques in addition to the standard COMP2111 lectures. The extended stream offers one additional hour of lectures per week on a voluntary basis. No additional assignments or assessment will be conducted in the extended stream. No additional credit will be offered. There are no prerequisites and the extended stream is open to all.

Parallel Teaching

None

Course Prerequisites

None

Course Exclusions

None

Constituents

  • Lecture: one hour per week in addition to normal COMP2111.
  • Tutorials: no additional tutorials.
  • Assignments: no additional assignments.

Preliminary Course Schedule

Week Topic
1 no lecture in extended stream
2 How do I build software that actually works? (Techniques overview and cool projects that did it)
3 What's in a proof? (Natural Deduction)
4 The proposition. (Propositional logic tools)
5 Vampires and other demons of the 1st order. (First order logic and automation)
6 Hey, check out this model! (SPIN and model checking)
7 A functional program? (Equations and recursion)
8 A symbolic execution. (Proof by term rewriting)
9 Induction, supernatural. (Proof by structural induction)
10 States and imperatives. (Pre- and post conditions, Hoare logic)
11 To vary or not to vary? (Invariants, proof about loops)
12 Terminate. Will it? (Proof of program termination)

Course philosophy and teaching strategies

The learning focus in this course is primarily on lectures and tool demonstrations. The extended stream of lectures is voluntary for interested students and gives a broader overview of formal modelling and proof techniques.

Assessment

There is no additional assessment for the extended stream.

Text and Reference Books

See the page on reading material.

Continual course improvement

This extended stream is running for the first time in Session 1, 2010. We are interested in your feedback.

Further information

  • Attendance for the COMP2111 extended stream is voluntary and open to all students.
  • The use of School of Computer Science and Engineering computing laboratories is subject to rules described in the Yellow Form, which you acknowledge (electronic) receipt of when you receive your computing account. The Yellow Form also outlines what to do in case illness or misadventure that affects your assessment, and supplementary examinations procedures within the School of Computer Science and Engineering.-->
  • UNSW Occupational Health and Safety policies and expectations.
  • Equity and Diversity.