Notices

  • W1 L2 video is up on webcms under Lectures

    Posted by Sebastian Sequoiah-Grayson Thursday 04 June 2026, 02:21:24 PM.

    Hi everyone - as per the subject header : )

  • You are welcome

    Posted by Sebastian Sequoiah-Grayson Thursday 04 June 2026, 09:22:09 AM.

    Hi : )

    Just ftr - if you are enrolled in the online lecture stream you are of course still very welcome to attend in-person.

    'til soon,

    Seb

  • Lecture video on webcms (youtube)

    Posted by Sebastian Sequoiah-Grayson Tuesday 02 June 2026, 03:41:17 PM, last modified Tuesday 02 June 2026, 03:45:41 PM.

    Hi everyone. Today's lecture video is now available on webcms under Lectures. I am exporting a colour-graded and audio-improved version from Davinci as I write this, but it takes hours to process. I shall upload it in the morning.

    (As predicted, the Echo 360 video is a disaster. Sorry. But it is funny to watch. The one on webcms is from my phone.)

    Most importnatly, thank you for all of your great questions today!!

  • Tutorial practice Qs added to webcms

    Posted by Sebastian Sequoiah-Grayson Tuesday 02 June 2026, 07:53:31 AM, last modified Tuesday 02 June 2026, 03:34:53 PM.

    Hi everyone : ) I have added some tutorial practice exercises for this week to webcms under Course Work. The idea is to have a read and a think and then you will work through them together in your tutorial with your tutor. It does not matter too much if you cannot get to them before the tutorial.

    The practices exercises DO NOT count towards your final mark in any way. They are just there to help you build up your skill sets with regard to creating and running your own verification environments. We start small, but some of them for Week 1 are deceptively tricky nonetheless. Have fun, and see you today at 11!


  • Updated lecture notes

    Posted by Sebastian Sequoiah-Grayson Monday 01 June 2026, 10:46:46 AM, last modified Monday 01 June 2026, 10:47:33 AM.

    With big thanks to Maxim Burykin for spotting two errors (the ommision of the base case in the inductive deifnintion of wffs, and an erroneous transformation of ~B into ~A in a tree-proof), the corrected lecture notes have been uploaded.

    There wll be more typos I promise : ) If you think that you have spotted one then please do post in the forum and I shall hop on to it.

    Thaks again Maxim, and see you all tomorrow for our first lecture!

    Seb

  • Lecture Notes are Live!

    Posted by Sebastian Sequoiah-Grayson Sunday 31 May 2026, 04:00:12 PM.

    Hi everyone!

    I am writing a book for you: Formal Reasoning: A Guide for Humans and Machines : )

    I have added a draft to webcms under <Lecture Notes>. I have added a Readings column to the Course Schedule section in the Course Outline.

    Truth be told, you can probably make it through the course without reading the readings (I can hear you cheering as I write this), but they are there to cover everything in detial.

    We are going to learn everything together by doing it together.

    See you soon!

    Seb

  • Welcome to COMP2111!

    Posted by Sebastian Sequoiah-Grayson Tuesday 26 May 2026, 01:06:36 PM.

    Aaaaaannnnnnnnd…let’s go!

    Welcome to the brand new COMP2111 - Foundations of Formal Methods : )

    Vineet and I are terribly excited about the whole thing really.

    You can find the course outline on webcms here:

    https://webcms3.cse.unsw.edu.au/COMP2111/26T2/outline

    Please do read the course outline. It has a lot of information in it with regard to due dates for assessments and other things. But due dates are terribly boring I know. Content however, is not!

    The first half of the course moves from propositional logic through to the Curry-Howard correspondence, via predicate logic, model theory, and intuitionistic/constructive logic. I know that some of you will be familiar with some of this whilst some of you will barely recall anythign from discrete maths. This does not matter. By the end of Week 2 everyone will be on the same page. I have done this before. Trust me : )

    The second half of the course will take you through all things formal methods, via Dafny. The point here is that by the time we get to Dafny and verification and functional programming and whatnot, you will understand why it all works the way that it it does, not only how. This matters.

    Vineet and I shall be giving the lectures. Edward is your course admin. Charran, Thomas, and Adam are your tutors.

    To preempt - you have four assignments and they are take-home. The exam is in labs. Again, all dates are in the course outline on webcms that you will of course be reading carefully. Right? Good.

    I shall be uploading lecture notes to webcms as they are ready. I am writing them as we go, which is exciting.

    Is there anythign else? I do not think so. At least not yet. Oh yes, please come to the lectures in person. It is more fun and you will learn more. There will be a lot of board work.

    Please do say hi below. Please do check the forum often. Please do help each other.

    All best,

    Seb


Back to top

COMP2111 26T2 (Foundations of Formal Methods) is powered by WebCMS3
CRICOS Provider No. 00098G