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
Tues 14:00 - 16:00 (K-B11B-8)
Thu 14:00 - 15:00 (CE G06)
6UOC and 3L+1T/L
To educate students on the concepts of algorithmic verification and give them hands-on experience in verification tools.
To educate students on
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.
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.
COMP3151 or COMP9151 or, enrolment in MIT program 8684 or GradCert program 7344, or permission from the lecturer in charge.
Classes in italics are planned to be held by Ansgar and in plain text by Ralf:
week | dates | content |
---|---|---|
1 | 28-02 and 2-03 | Introduction |
2 | 7-03 and 9-03 | Modelling Systems |
3 | 14-03 and 16-03 | Temporal Logic |
4 | 28-03 and 30-03 | CTL Model Checking |
5 | 28-03 and 30-03 | NuSMV |
6 | 04-04 and 6-04 | LTL Model Checking |
7 | 11-04 and 13-04 | Spin |
8 | 18-04 and 20-04 | recess |
9 | 25-04 and 27-04 | Anzac day and project session |
10 | 2-05 and 4-05 | Partial order and symmetry reduction |
11 | 9-05 and 11-05 | SAT-based model checking |
12 | 16-05 and 18-05 | Static Analysis |
13 | 23-05 and 25-05 | Model checking Timed Automata |
14 | 30-05 and 1-06 | Beyond time |
15 | 6-06 and 8-06 | Summary and Discussion |
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.
topSupplementary 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.
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