Introduction

It is virtually impossible to guarantee correctness of a system, and in turn the absence of bugs by standard software engineering practice such as code review, systematic testing and good software design alone. The complexity of systems is typically too high to be manageable by informal reasoning or reasoning that is not tool supported. The formal methods community has developed various rigorous, mathematically sound techniques and tools that allow the automatic analysis of systems and software. The application of these fully automatic techniques is typically called algorithmic verification.

The course will describe several automatic verification techniques, the algorithms they are based on, and the tools that support them. We will discuss examples to which the techniques have been applied, and provide experience with the use of several tools.

top

Administrative

Lecturer

When and Where

Tues 14:00 - 16:00 (K-B11B-8)
Thu 14:00 - 15:00 (CE G06)

Credit Value and Mode of Instruction

6UOC and 3L+1T/L

Course Goal

To educate students on the concepts of algorithmic verification and give them hands-on experience in verification tools.

Technical

To educate students on

Educational

Expose students to a scientific theory of algorithmic verification techniques, the underlying concepts for state-of-the-art tools, and sound frameworks for program analysis.

Course philosophy and teaching strategies

The learning focus in this course is primarily on lectures and assignments, plus a mid term project which you can use to demonstrate your skills acquired until then. While marks are assigned to the assignments, their primary purpose is to give you concrete tasks with deadlines to help you structure your learning.

Prerequisite

COMP3151 or COMP9151 or, enrolment in MIT program 8684 or GradCert program 7344, or permission from the lecturer in charge.

Assessment Criteria

top

Content

Classes in italics are planned to be held by Ansgar and in plain text by Ralf:

weekdatescontent
128-02 and 2-03Introduction
27-03 and 9-03Modelling Systems
314-03 and 16-03Temporal Logic
428-03 and 30-03CTL Model Checking
528-03 and 30-03NuSMV
604-04 and 6-04LTL Model Checking
711-04 and 13-04Spin
818-04 and 20-04recess
925-04 and 27-04Anzac day and project session
102-05 and 4-05Partial order and symmetry reduction
119-05 and 11-05SAT-based model checking
1216-05 and 18-05Static Analysis
1323-05 and 25-05Model checking Timed Automata
1430-05 and 1-06Beyond time
156-06 and 8-06Summary and Discussion

top

Literature

A great part of the lecture is covered in: Model Checking, Edmund Clarke, Orna Grumberg and Doron Peled, MIT Press 2000. This textbook can be obtained at the UNSW bookshop. For futher reading see the Resources section.

top

Formal Notices

Supplementary Exam

Supplementary exams will only be awarded in well justified cases, in accordance with School policy, not as a second chance for poor performance. In particular, it is unlikely that a supplementary will be awarded to students who have actually sat the proper exam.

Supplementary exams will be oral. The supplementary final exam will be held after the written supplementary exams held for other courses.

Pointers to Important Information

Continual course improvement

Student feedback on this course, and on the lecturing in this course, will be gathered via questionnaires held at or after the end of the course. Student feedback is taken seriously, and continual improvements are made to the course based in part on this feedback. The course questionnaire results go to the Head of the School of Computer Science and Engineering, who reads the results and follows up in cases where action is clearly needed.

CRICOS Provider Number: 00098G