- Class Number 7608
- Term Code 3260
- Class Info
- Unit Value 6 units
- Topic Algorithmic Verification
- Mode of Delivery In Person
- Peter Hoefner
- Peter Hoefner
- Class Dates
- Class Start Date 25/07/2022
- Class End Date 28/10/2022
- Census Date 31/08/2022
- Last Date to Enrol 01/08/2022
- Jack Stodart
This course is available so that senior students can pursue, with a small class, topics that are not covered in the regular curriculum that will significantly increase their knowledge of some aspect of computer science.
The activities in the course will be a combination of lectures, workshops, reading, writing and project work, as appropriate to the topic. These activities will be specified in separate websites for each class.
Upon successful completion, students will have the knowledge and skills to:
- Learning Outcomes will be determined for each individual student and recorded in an 'Independent Study Contract' at the beginning of the course.
Whether you are on campus or studying remotely, there are a variety of online platforms you will use to participate in your study program. These could include videos for lectures and other instruction, two-way video conferencing for interactive learning, email and other messaging tools for communication, interactive web apps for formative and collaborative activities, print and/or photo/scan for handwritten work and drawings, and home-based assessment.
ANU outlines recommended student system requirements to ensure you are able to participate fully in your learning. Other information is also available about the various Learning Platforms you may use.
Students will be given feedback in the following forms in this course:
- written comments
- verbal comments
- feedback to whole class, groups, individuals, focus group etc
ANU is committed to the demonstration of educational excellence and regularly seeks feedback from students. Students are encouraged to offer feedback directly to their Course Convener or through their College and Course representatives (if applicable). Feedback can also be provided to Course Conveners and teachers via the Student Experience of Learning & Teaching (SELT) feedback program. SELT surveys are confidential and also provide the Colleges and ANU Executive with opportunities to recognise excellent teaching, and opportunities for improvement.
Hurdle: students must achieve an average of 40% in their take-home assignments (Homework 1-4), and also 40% in the final exam to pass the course.
|Week/Session||Summary of Activities||Assessment|
|1||Temporal Logics: LTL and CTL 1) Syntax 2) Semantics 3) Expressiveness||These units introduce the logical language, which is the basis for the course. They are used to specify formal systems.|
|2||Automata (Finite State Machines)||This unit is a recapitulation of material presented in COMP1600/COMP6260. Automata are the basis to model computer systems formally.|
|3||Reachability and Safety||Simple properties of systems (modelled as automata) are reachability and safety. These units illustrate how properties can be checked. First tools are introduced|
|4||CTL Model Checking 1) Classic Model Checking Algorithm 2) Abstraction and Refinement 3) Symbolic CTL Model Checking||These units illustrate how specifications written in CTL can be automatically checked; tools supporting these approaches are discussed.|
|5||LTL Model Checking via Büchi Automata||These units illustrate how specifications written in LTL can be automatically checked; tools supporting these approaches are discussed.|
|6||Limits of Model Checking 1) Bounded Model Checking 2) Predicate Abstraction Refinement||These units illustrate limits of model checking approaches and illustrates solutions based on finite boundaries and predicate abstraction|
|7||Static Analysis 1) Data Flow Analysis 2) Fixed Points 3) Available Expression Analysis 4) Abstract Interpretation [optional]||These units introduce strategies different from model checking; guest lecturers are envisioned for these topics (can only be confirmed closer to the dates of the lectures)|
|8||Timed Model Checking 1) Timed and Region Automata 2) Timed Languages 3) Timed Logics and Model Checking||These units extend classical model checking approaches by time; as standard in this lecture industrial tools are discussed.|
|Assessment task||Value||Due Date||Learning Outcomes|
|Homework 0||5 %||05/08/2022||2,4|
|Homework 1||9 %||23/08/2022||2,3,4|
|Homework 2||11 %||19/09/2022||1,2,5|
|Homework 3||11 %||11/10/2022||1,2,4,5,6|
|Homework 4||9 %||01/11/2022||1,2,4,6|
|Final Exam||55 %||*||1-6|
* If the Due Date and Return of Assessment date are blank, see the Assessment Tab for specific Assessment Task details
ANU has educational policies, procedures and guidelines , which are designed to ensure that staff and students are aware of the University’s academic standards, and implement them. Students are expected to have read the Academic Integrity Rule before the commencement of their course. Other key policies and guidelines include:
- Academic Integrity Policy and Procedure
- Student Assessment (Coursework) Policy and Procedure
- Special Assessment Consideration Guideline and General Information
- Student Surveys and Evaluations
- Deferred Examinations
- Student Complaint Resolution Policy and Procedure
- Code of practice for teaching and learning
The ANU is using Turnitin to enhance student citation and referencing techniques, and to assess assignment submissions as a component of the University's approach to managing Academic Integrity. For additional information regarding Turnitin please visit the Academic Skills website. In rare cases where online submission using Turnitin software is not technically possible; or where not using Turnitin software has been justified by the Course Convener and approved by the Associate Dean (Education) on the basis of the teaching model being employed; students shall submit assessment online via ‘Wattle’ outside of Turnitin, or failing that in hard copy, or through a combination of submission methods as approved by the Associate Dean (Education). The submission method is detailed below.
Moderation of Assessment
Marks that are allocated during Semester are to be considered provisional until formalised by the College examiners meeting at the end of each Semester. If appropriate, some moderation of marks might be applied prior to final results being released.
Assessment Task 1
Learning Outcomes: 2,4
To support on-going learning of the course content, five individual take-home assignments (homework) are given, distributed over the entire semester. This is the first. Students will get exercises related to the course content discussed so far and will have at least 10 days to submit their answer.
Assessment Task 2
Learning Outcomes: 2,3,4
To support on-going learning of the course content, five individual take-home assignments (homework) are given, distributed over the entire semester. This is the second. Students will get exercises related to the course content discussed so far and will have at least 10 days to submit their answer.
Assessment Task 3
Learning Outcomes: 1,2,5
To support on-going learning of the course content, five individual take-home assignments (homework) are given, distributed over the entire semester. This is the third. Students will get exercises related to the course content discussed so far and will have at least 10 days to submit their answer.
Assessment Task 4
Learning Outcomes: 1,2,4,5,6
To support on-going learning of the course content, five individual take-home assignments (homework) are given, distributed over the entire semester. This is the forth. Students will get exercises related to the course content discussed so far and will have at least 10 days to submit their answer.
Assessment Task 5
Learning Outcomes: 1,2,4,6
To support on-going learning of the course content, five individual take-home assignments (homework) are given, distributed over the entire semester. This is the fifth. Students will get exercises related to the course content discussed so far and will have at least 10 days to submit their answer.
Assessment Task 6
Learning Outcomes: 1-6
The final exam will be held either orally or in written form. An oral exam is the preferred mode of delivery, but depending on the class size a "classical" written exam may be required. The mode of delivery is clearly communicated in the first week of lectures.
Oral exams test the students' knowledge (regarding the content of the course) in form of questions or small tasks to be performed.
Academic integrity is a core part of the ANU culture as a community of scholars. The University’s students are an integral part of that community. The academic integrity principle commits all students to engage in academic work in ways that are consistent with, and actively support, academic integrity, and to uphold this commitment by behaving honestly, responsibly and ethically, and with respect and fairness, in scholarly practice.
The University expects all staff and students to be familiar with the academic integrity principle, the Academic Integrity Rule 2021, the Policy: Student Academic Integrity and Procedure: Student Academic Integrity, and to uphold high standards of academic integrity to ensure the quality and value of our qualifications.
The Academic Integrity Rule 2021 is a legal document that the University uses to promote academic integrity, and manage breaches of the academic integrity principle. The Policy and Procedure support the Rule by outlining overarching principles, responsibilities and processes. The Academic Integrity Rule 2021 commences on 1 December 2021 and applies to courses commencing on or after that date, as well as to research conduct occurring on or after that date. Prior to this, the Academic Misconduct Rule 2015 applies.
The University commits to assisting all students to understand how to engage in academic work in ways that are consistent with, and actively support academic integrity. All coursework students must complete the online Academic Integrity Module (Epigeum), and Higher Degree Research (HDR) students are required to complete research integrity training. The Academic Integrity website provides information about services available to assist students with their assignments, examinations and other learning activities, as well as understanding and upholding academic integrity.
You will be required to electronically sign a declaration as part of the submission of your assignment. Please keep a copy of the assignment for your records. Unless an exemption has been approved by the Associate Dean (Education) submission must be through Turnitin.
For some forms of assessment (hand written assignments, art works, laboratory notes, etc.) hard copy submission is appropriate when approved by the Associate Dean (Education). Hard copy submissions must utilise the Assignment Cover Sheet. Please keep a copy of tasks completed for your records.
Late submission not permitted. If submission of assessment tasks without an extension after the due date is not permitted, a mark of 0 will be awarded.
The Academic Skills website has information to assist you with your writing and assessments. The website includes information about Academic Integrity including referencing requirements for different disciplines. There is also information on Plagiarism and different ways to use source material.
Extensions and Penalties
Extensions and late submission of assessment pieces are covered by the Student Assessment (Coursework) Policy and Procedure. Extensions may be granted for assessment pieces that are not examinations or take-home examinations. If you need an extension, you must request an extension in writing on or before the due date. If you have documented and appropriate medical evidence that demonstrates you were not able to request an extension on or before the due date, you may be able to request it after the due date.
Distribution of grades policy
Academic Quality Assurance Committee monitors the performance of students, including attrition, further study and employment rates and grade distribution, and College reports on quality assurance processes for assessment activities, including alignment with national and international disciplinary and interdisciplinary standards, as well as qualification type learning outcomes.
Since first semester 1994, ANU uses a grading scale for all courses. This grading scale is used by all academic areas of the University.
Support for students
The University offers students support through several different services. You may contact the services listed below directly or seek advice from your Course Convener, Student Administrators, or your College and Course representatives (if applicable).
- ANU Health, safety & wellbeing for medical services, counselling, mental health and spiritual support
- ANU Access and inclusion for students with a disability or ongoing or chronic illness
- ANU Dean of Students for confidential, impartial advice and help to resolve problems between students and the academic or administrative areas of the University
- ANU Academic Skills and Learning Centre supports you make your own decisions about how you learn and manage your workload.
- ANU Counselling Centre promotes, supports and enhances mental health and wellbeing within the University student community.
- ANUSA supports and represents undergraduate and ANU College students
- PARSA supports and represents postgraduate and research students