CS476: Program Verification

Fall 2023

Topic List

Course Work, Policies and Procedures

Students taking the course will be expected to:


Reading Materials


Lecture 1 (22nd Aug)

Lecture 2 (24th Aug)

Lecture 3 (29th Aug)

Lecture 4 (31st Aug)

Lecture 5 (5th Sept)

Lecture 6 (7th Sept)

Lecture 7 (12th Sept)

Lecture 8 (14th Sept)

Lecture 9 (19th Sept)

Lecture 10 (21st Sept)

Lecture 11 (26th Sept)

Lectures 12 (28th Sept)

Lecture 13 (3rd Oct)

Lecture 14 (5th Oct)


When submitting homework please make sure:

  1. All homework is typed.

    Homework will not be accepted if it is not typed.

  2. All attachments should start with cs476-hwN-<netid>.

    For example, cs476-hw2-clarage2.pdf, or cs476-hw2-clarage2-nat-list.maude.

    Ten precent will be deducted if you do not use this naming format. I will likely not be able to find your assignment in my email if you don’t use this format.

    Make sure you use hypens and not underscores.

  3. Place your name and netid in the title or header of the PDF. This is to ensure that your homework doesn’t get mixed up with someone else’s.

HW1 (Due 29th Aug)

HW2 (Due 5th Sept)

HW3 (Due 12th Sept)

Due to an error, Homework 3 has been changed as of September 5th 8pm. Please use this latest version of Homework 3 and discard any prior version.

HW4 (Due 19th Sept)

HW5 (Due 26th Sept)

HW6 (Due 3rd Oct)

HW7 (Due 10th Oct)

Tools used


Maude will be the primary tool used in this course, but several tools/libraries written in Maude will also be used. It may be downloaded from the github release page and installed as per instructions at the Maude wiki.

Instructions for usage on EWS (Maude 3.1)

The EWS machines have an older version of glibc, so we must use Maude 3.1 instead of the latest available version. Below are instructions to download and install that version.

$ wget http://maude.cs.illinois.edu/w/images/3/38/Maude-3.1-linux.zip
$ unzip Maude-3.1-linux.zip
$ cd maude-3.1/
$ ./maude.linux64
./maude.linux64: /lib64/libtinfo.so.5: no version information available (required by ./maude.linux64)
           --- Welcome to Maude ---
         Maude 3.1 built: Oct 12 2020 20:12:31
         Copyright 1997-2020 SRI International
           Mon Aug 29 11:15:24 2022

Instructions for usage on newer versions of Linux (Maude 3.2.1)

# Download and unzip Maude binary release for Linux
$ wget https://github.com/SRI-CSL/Maude/releases/download/3.2.1/Maude-3.2.1-linux.zip
$ unzip Maude-3.2.1-linux.zip
# Run Maude
$ cd Linux64/
$ ./maude.linux64
                  --- Welcome to Maude ---
           Maude 3.2.1 built: Feb 21 2022 18:21:17
            Copyright 1997-2022 SRI International
                  Mon Aug 29 18:20:44 2022

Instructions for usage on MacOS (Maude 3.2.1)

# Download and unzip Maude binary release for MocOS
$ wget https://github.com/SRI-CSL/Maude/releases/download/3.2.1/Maude-3.2.1-macos.zip
$ unzip Maude-3.2.1-macos.zip
# Run Maude
$ cd Darwin64/
$ ./maude.darwin64
                  --- Welcome to Maude ---
           Maude 3.2.1 built: Feb 21 2022 18:21:17
            Copyright 1997-2022 SRI International
                  Mon Aug 29 18:20:44 2022

Maude Formal Environment (MFE)

The MFE packages together several tools which will be used in the course. It's recommended that you use the binary releases for anything needing the MFE. To get setup using MFE, you might do:  

# Clone MFE
$ git clone 'https://github.com/maude-team/mfe'

# Launch Maude with MFE
$ ./maude mfe/src/mfe.maude

--- Welcome to Maude ---
maude 2.7.1 built: Aug 31 2016 18:22:38
copyright 1997-2016 SRI International
sun Oct 1 11:51:55 2017

full Maude 2.7e September 22th 2016

the Maude Formal Environment 1.0b
inductive Theorem Prover - July 20th 2010
sufficient Completeness Checker 2a - August 2010
church-Rosser Checker 3p - August 30th 2016
coherence Checker 3p - August 30th 2016
maude Termination Tool 1.5j - August 11th 2014


Note that many of the tools in the MFE cannot reason with built-in modules (many of the modules which come in prelude.maude). By default though, Maude includes the built-in module BOOL with any user-defined module. If you get the following error:

Error The use of built-ins is not supported by the checker.

be sure to disable including BOOL into your module by default:

set include BOOL off .

fmod MYMODULE is

If you are in loop mode (eg. if you have already loaded the MFE), then you must do this in parentheses instead:

(set include BOOL off .)

(fmod MYMODULE is

Sufficient Completeness Checker

The SCC tool works on an older version of Maude, and I only know of Linux binaries for it. Login to EWS or use a virtual machine if you are not on a Linux machine.

$ wget 'http://maude.cs.uiuc.edu/tools/scc/releases/Maude-ceta-2.3-linux.tgz'
$ tar -xvf Maude-ceta-2.3-linux.tgz
$ cd Maude-ceta-2.3-linux
$ ./maude-ceta

--- Welcome to Maude ---
Maude-ceta 2.3 built: Feb 18 2007 09:49:47
Copyright 1997-2007 SRI International
With CETA extensions Copyright 2006-2007
University of Illinois at Urbana-Champaign
Mon Oct 2 19:17:22 2017

# Load SCC
Maude> load scc.maude

# Start the SCC
Maude> loop init-cc .
Starting the Maude Sufficient and Canonical Completeness Checker.

# Load the file with module of interest (note that it should NOT be in parens)

# Select the CC-LOOP module.
Maude> select CC-LOOP .

# Check Sufficient Completeness (modulo other proof goals)
Warning: no loop state.
Advisory: attempting to reinitialize loop.
Starting the Maude Sufficient and Canonical Completeness Checker.
Checking sufficient completeness of MODULE-OF-INTEREST ...
Success: MODULE-OF-INTEREST is sufficiently complete under the assumption that it is ground weakly-normalizing, confluent, and ground sort-decreasing.

NuITP (Interactive theorem prover)

The NuITP, https://nuitp.webs.upv.es/, may be downloaded from here and works with Maude 3.3.1. The manual has instructions for using the using the prover.

LMC (Logical Model Checker)

The Maude Logical Model checker may be downloaded from here. The zip archive includes a customized version of Maude. It is required that you use this version.

Note: This is compiled only for Linux and MacOS on Intel. If you are using Windows or a newer OSX machine, please use the EWS machines to run the Linux binary.

To check that a property is valid, we create a file, my-module-check.maude in the following format:

--- Code to define/load the module we are testing goes here.
load my-module

--- Load the symbolic model checker
load symbolic-checker

--- In a module that extends the SYMBOLIC-CHECKER module and protects the Module to be tested, we:
--- 1. Define the states over which traces are defined by adding a subsort to the State sort.
--- 2. Define labels over the states as constructors in the Prop sort.
--- 3. Add equations over the |= operator to define the set of labels for a state.

( mod MY-PREDS is
    extending SYMBOLIC-CHECKER .
    protecting MY-MODULE .

    subsort MyState < State .
    ops label1 label2 : -> Prop [ctor] .

    eq MyState |= label1 = true [variant] .

endm )

--- Check that an LTL property is valid
( lfmc InitState |= LTLFormula1 . )
( lfmc InitState |= LTLFormula2 . )

and run:

$ ./maude.linux64 my-module-check.maude