CS476: Program Verification

Fall 2022

Topic List

Course Work, Policies and Procedures

Students taking the course will be expected to:

Grading.

Reading Materials

Lectures

Lecture 1 (23rd Aug)

Lecture 2 (25th Aug)

Lecture 3 (30th Aug)

Lecture 4 (1st Sept)

Lecture 5 (6th Sept)

Lecture 6 (8th Sept)

Lecture 7 (13th Sept)

Lecture 8 (15th Sept)

Lecture 9 (20th Sept)

Lecture 10 (22th Sept)

Lecture 11 (29th Sept)

Lecture 12 (4th Oct)

Lecture 13 (6th Oct)

Lecture 14 (11th Oct)

Lecture 15 (18th Oct)

Lecture 16 (20th Oct)

Lecture 17 (25th Oct)

Lecture 18 (27th Oct)

Lecture 19 (1st Nov)

Lecture 20 (3rd Nov)

Lecture 21 (10th Nov)

Lecture 22 (15th Nov)

Lecture 23 (17th Nov)

Lecture 24 (29th Nov)

Lecture 25 (1st Dec)

Lecture 26 (6th Dec)

Homework

When submitting homework please make sure:

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

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

    From HW4 onward, two points will be deducted if you do not use this 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.

  2. 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 1st Sept)

HW2 (Due 8th Sept)

HW3 (Due 15th Sept)

HW4 (Due 22th Sept)

HW5 (Due 29th Sept)

HW6 (Due 6th Oct)

HW7 (Due 13th Oct)

HW8 (Due 20th Oct)

HW9 (Due 27th Oct)

HW10 (Due 03rd Nov)

HW11 (Due 10th Nov)

HW12 (Due 17th Nov)

HW13 (Due 1st Dec)

Comprehensive Homework (Due Dec 12)

Tools used

Maude

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
Maude>

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
Maude>

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

maude>

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
    ...
endfm

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
    ...
 endfm)

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)
Maude> load ../../../PATH/TO/FILE/WITH/MODULE/NOT/IN/PARENTHESES

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

# Check Sufficient Completeness (modulo other proof goals)
Maude> (scc MODULE-OF-INTEREST .)
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 may be downloaded from here and works with Maude 3.2.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