Algorithmic Verification COMP3153/COMP9153 25T3

Exam information

Posted by Paul Hunter Wednesday 03 December 2025, 08:52:30 PM.

Hi all,

Apologies for the long silence - I have been dealing with a few issues at my end.

Hopefully you have received details of when & where the COMP3153/9153 exam is held tomorrow -- please note students will be spread across several rooms, so do not assume your room is the same as others. I should be on hand at the start to answer any questions.

I have had some queries about exam specifics, here is a quick rundown of the basics that I believe you need to know:

* The exam is 2 hours in duration
* There are 7 questions (approximately equally weighted). Questions are similar to past exams (which have been available on the course website) though only covering the content we covered this year (also, Model Checking Knowledge will not be examined). Please note that past exams were 24 hour take-home exams, so the level of detail asked (and expected in solutions) will be adjusted accordingly.
* Allowed materials are one A4 page (double sided) of notes . There is no other restriction on these notes (i.e. they may be typed, handwritten etc). You should not need (nor bring) anything else other than pens/pencils and student ID (i.e. no calculators).
* You will be provided with two answer booklets; please answer in the answer booklets, starting each question on a new page .

I will keep you posted if there is anything more that comes up.

Best of luck tomorrow,

Paul

mck2 shared libraries

Posted by Ron Van der Meyden Wednesday 12 November 2025, 12:29:53 AM.

The new mck2 binary needs some shared libraries, it turns out.

On CSE servers, try

export LD_LIBRARY_PATH="/import/reed/3/mck/lib:$LD_LIBRARY_PATH"

and then run mck2, or copy the libraries at that location to your own machine and use a similar command so that they can be found.

New version of MCK

Posted by Ron Van der Meyden Tuesday 04 November 2025, 05:03:25 PM.

I have placed a new version of MCK at ~mck/bin/mck2 on CSE servers.

This is the current development version, with some improvements to the input language:

-- multi-dimensional arrays

- indexing arrays by enumerated types (replacing arrays of unspecified size)

- quantification (treated as a macro)

- new atomic statements <| non-looping code | non-looping code |>

- several choices of transition semantics (including turn-based for modeling asynchrony)

See the draft manual in the Coding Examples block below for more detail on the new features.

This version is still a work in progress, but there should be fewer bugs in the parts that are working, and better type checker error messages. The bug relating to enumerated types in the explicit state game has been fixed, BDD based model checking works, bounded model checking works (with a new SMT based version also). That should cover what we need in COMP3153.

Some features like probability and the game for bounded model checking are disabled or not yet working correctly in this version, but these will not be covered in this course. Some of the old syntax (read/write in atomic actions in protocols) does not work since the new atomic actions replace this, but with a somewhat different semantics. (If you need asynchrony, use the turn-based semantics instead.)

I'll try to cover some examples of the new features in the lecture on Thus this week.