Algorithmic Verification COMP3153/COMP9153 25T3

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.

Welcome to COMP3153/9153

Posted by Paul Hunter Tuesday 16 September 2025, 12:02:57 PM, last modified Tuesday 16 September 2025, 12:19:06 PM.

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 be fully face-to-face for all learning aspects. 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 today at 14:00 in Ainsworth G02. 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 - no prior work is needed for the first tutorial, however for this first week please come along to the start of least one tutorial (see webCMS for the tutorial details) as I will be clarifying how assessments and tutorials will work through the term, and setting you all up for the main assessments. Ronald, Dao and Ye Li will be the tutorial team for this term.

The course will be using the discourse platform for course discussion. Please click here to join the forum.

The course will also be using the formatif platform for weekly assessment tasks. Details will follow in the first lecture and in the subsequent tutorials.

Looking forward to meeting you later,

Paul Hunter
(Course Convenor)

PS While you wait for the lecture to start, have a think about what is wrong with the following code fragment released on Ethereum a few years ago:

transfer(account to, account from, uint amount){
    require (balances[from] > amount);
    balancesFrom := balances[from] - amount;
    balancesTo := balances[to] + amount;
    balances[from] := balancesFrom;
    balances[to] := balancesTo;
}