Hi all,
There are a couple of typos on the exam that shouldn't have too much of an impact but can lead to some unnecessary ambiguity.
Q4 had the CTL and LTL subscripts the wrong way around [this has now been fixed]
Q10 a iv should read: "In the next 3 time units: there will be an a followed by (at some point) a b followed by (at some point) a c." (I.e. there should be a colon and a clarification about "followed by"). [this has now been fixed]
Update:
Q10 b should read: "Express, or show that it is not possible to express, the properties in (a) in MTL (or TCTL)" [this has now been fixed]
If there are any other sources of ambiguity then you should exercise your own judgement, but clearly state the interpretation you are adopting, so you don't get unfairly penalised for what might be a reasonable interpretation.
Paul
Hi all,
The final exam is now available on the course website under "Exam Resources". It is due at
9am Friday 19 August (AEST)
.
As with assignments, you can submit as often as you like - your last submission before the deadline will be what is marked.
I have also included, on the course webpage, the LaTeX code for all automata that appear in the exam to make it easier to draw some of the diagrams (if needed).
I have just realised that the assignment solutions were not posted - I'll get them out onto the website asap.
Good luck,
Paul
Hi all,
For today's lecture, Ron van der Meyden will (hopefully) be giving a guest lecture on some of the work he is involved in - specifically Model Checking for Epistemic Logic (Logic of "Information Flow"). The lecture will be on zoom as usual.
For tomorrow's lecture, I have organised a room on campus: G23 in the Law Building (F8). It is a hybrid room, so I should be able to livestream, as well as record the lecture - but it would be great if those of you that are able (and willing) to come for a final face-to-face meeting. We will be reviewing the course and I'll be answering any questions you have, including about the final exam.
Looking forward to seeing you,
Paul
Hi all,
The fourth assignment is now available. It is due on
Monday 8th August at 17:00.
Please note that because of the reduced timeframe, the workload required for the assignment has been adjusted accordingly.
Paul
Hi all,
The spec for Part B of Assignment 3 is now available on the course website. There are some presentation issues that I will clear up later, but I thought I'd better get it out to you asap.
I will set up the give submission later today.
Paul
Hi all,
The first half of Assignment 3 [the theory aspect] is now available on the course website. It is due on
Friday 29 July
at
17:00
.
I am still finalizing the spec for the second part [practical aspect] and will release it later tonight. If you are keen to start working on it, it will be asking you to "solve" the "Wolf-Goat-Cabbage river crossing problem" using Spin - so have a think about how you might go about solving that.
Paul
Hi everyone!
A reminder that tomorrow's tutorial is online and not in-person since I tested positive for COVID-19. We'll be using the Tuesday 14:00 Zoom link which you can find here ; hope to see you all (virtually) there!
- Gerald
Hi all,
Apologies for the late notice, but Moshe Vardi (one of the foremost researchers in Formal Verification, and an excellent speaker) will be giving a live-streamed presentation (which I believe we should be able to access) from a Formal Verification workshop in the UK from
11:30pm tonight
.
His talk is titled "Program Verification: a 70+ year history" so it should be accessible to all students in this course.
The stream (if it is available) can be found here:
https://www.newton.ac.uk/news/watch-live/
Paul
Hi all,
We had enough interest for me to do a recap lecture in flex week. There was no preferred day, so I'll hold it on Wednesday at 10am - via zoom, as usual.
Paul
Hi all,
I've added a poll to the course website to see if enough people would be interested in a lecture next week to recap the contents of Weeks 1-5. If there is enough interest, I will run one at the most popular time. It will be recorded for those that cannot make it.
Paul
Hi all,
The second assignment is now available. It is due on
Friday 1 July
at
17:00
(AEST).
Note that content for the last part will be covered on Wednesday this week.
Tuesday's lecture will be online as usual because we will be covering SPIN/Promela, and it is easier to do this in an online setting than f2f.
Paul
Hi all,
At the end of my slides for Lecture 4 I forgot to put in a bibliography and a link/reminder for the weekly feedback . I have now added these to the uploaded slides.
Also a reminder that the lecture on Tuesday next week will be on campus in Ainsworth 202 at 11-1. It'd be great to meet as many of you as I can, and to encourage participation at the somewhat inconvenient time I'll be shouting [some form of] lunch for the attendees. To work out what sort of lunch, I've set up a poll:
https://forms.office.com/r/S3sgVySUUq
Please consider sharing your opinion, even if you are only a maybe. The poll will finish at 2pm tomorrow (Saturday) so that I have time to organise whatever option is most popular.
Looking forward to meeting those of you who can make it,
Paul
Apologies - I accidentally uploaded the wrong spec earlier on. The correct assignment spec is now available.
Hi all,
The first assignment is now available on the course website. It is due on
Friday 17th June
at
17:00 (AEST)
. I will shortly add the LaTeX source code for the automata (under Course work → Assignments).
Please submit your solutions as a single pdf via webCMS/give.
I have just realised that I did not mention late penalties in the lectures. I will be following the standard UNSW late penalty policy which has come into effect just recently. This is a penalty of 5% (of the total mark) per 24 hours or part thereof up to 5 days late.
Paul
Hi all,
Welcome to COMP3153/9153 - Algorithmic Verification. This is just a brief announcement to introduce you to various aspects of the course: the website, the learning interfaces, and the staff.
This term COMP3153/9153 will have a mix of online (for most content) and face-to-face delivery (for some tutorials). I encourage you to familiarise yourself with the course website:
http://www.cse.unsw.edu.au/~cs3153
as it provides the starting point for all aspects of the course.
Lectures begin on Tuesday (May 31) [i.e. tomorrow] at 11:00 and will be delivered in real time on Zoom. Details of the lectures can be found on the course website once you have logged in to webCMS. Lectures will be recorded, and the recording will be available shortly after the lecture finishes. No assurance is made about the quality/completeness of the recording - so the only way to ensure you have best lecture experience is to attend the lectures!
Tutorials begin in Week 1
. The Tuesday tutorial is online. The tutorial on Thursday will be face-to-face. Gerald Huang will be the tutor for all tutorials this term. Details of the online tutorial can be found on the course website.
The online tutorial will not be recorded.
Although there are lab sessions timetabled, for the time being there will be no scheduled labs. This may change later in the term if it is felt that there is a need for structured lab sessions.
The first set of tutorial questions are now available on the course website. These questions are intended to give an indication of the background knowledge that is recommended to get the most out of this course, so please attempt to work through them before the tutorial. While it is not necessary to be able to solve any of the questions before the tutorial, you should be comfortable with all concepts covered following the tutorial and this week's lectures.
The course will be using the ed platform for course discussion. You should shortly be receiving an email inviting you to join the ed forum for this course.
Looking forward to virtually meeting you tomorrow,
Paul Hunter
(Lecturer in Charge)