CS476: Program Verification

Fall 2023

Time: Tuesday and Thursday, 9:30AM - 10:45AM
Location: 101 Transportation Building (104 S Mathews Ave, Urbana, IL 61801)
Professor: José Meseguer
TA: Ben Clarage (email: clarage2@illinois.edu)
Course-Related Email: All course-related email for both the instructor and the TA should be sent to clarage2@illinois.edu

Topic List

Algebraic specification of declarative deterministic programs
Inductive first-order logic and inductive theorem proving verification of declarative deterministic programs.
Rewriting logic specification of declarative concurrent programs
Modal and temporal logic checking verification of declarative concurrent programs
Rewriting logic semantics of imperative concurrent programs
Model checking verification of imperative concurrent programs
Symbolic model checking and theorem proving verification of declarative concurrent programs

Course Work, Policies and Procedures

Students taking the course will be expected to:

Participate actively and regularly in the course.
Present answers to weekly homework assignments solved individually. Although student interaction and cooperation is encouraged, this excludes any communication on how to solve posted homework assignments, including the comprehensive one (see below). Communication on how to solve homework would constitute a serious violation of the honor code.
A comprehensive homework assignment at the end of the course.
(if the course is taken for 4 units) Develop a term project, either individually or as part of a small group of students.

Grading.

The regularity in active participation will contribute 20% to the final grade.
Each problem on each weekly homework assignment will be worth 10 points, and the weekly homeworks all together will be worth 60% of the grade.
Late homework will receive a 0%.
The final comprehensive homework assignment will be worth 20% of the grade.
There will be no final exam.
If you are taking the class for 4 credits, then there will also be a final project for the course. The final project must be turned in by the assigned final date before a grade for the class will be issued.

Reading Materials

(STACS) Set Theory and Algebra in Computer Science
Peter Olveczky's book Formal Modeling and Analysis of Distributed Systems
Algebraic Semantics of Imperative Programs, by Goguen, Malcolm
Maude Manual
All About Maude
Programming and Symbolic Computation in Maude
Maude Termination Assistant The MTA tool and a collection of examples can be found on the MTA website

Lectures

Lecture 13 (3rd Oct)

Lecture 14 (5th Oct)

Slides

Lecture 15 (10th Oct)

Lecture 16 (12th Oct)

Slides

Lecture 17 (17th Oct)

Slides

Lecture 18 (19th Oct)

Slides

Lecture 19 (24th Oct)

Slides

Lecture 20 (26th Oct)

Slides

Lecture 21 (31st Oct)

Lecture 22 (2nd Nov)

Slides

Lecture 23 (7th Nov)

Lecture 24 (9th Nov)

Lecture 25 (14th Nov)

Slides

Lecture 26 (16th Nov)

Lecture 27 (28th Nov)

Slides
[Appendix 1 - Not Completed Yet]
Appendix 2 on Abstract Logical Model Checking of Infinite-State Systems Using Narrowing

Lecture 28 (30th Nov)

Slides

Lecture 29 (5th Dec)

Slides

Homework

When submitting homework please make sure:

All homework is typed and submitted by the end of class Tuesday.

Homework will not be accepted if it is late or not typed.
All attachments should start with cs476-hwN-<netid>.

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

Ten percent 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 hyphens and not underscores.
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)

Homework 1

HW2 (Due 5th Sept)

Homework 2
Maude Source You should use this to copy the “skeleton” Maude code.

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.

Homework 3
Maude Source You should use this to copy the “skeleton” Maude code.

HW4 (Due 19th Sept)

Homework 4
Maude Source You should use this to copy the “skeleton” Maude code.

HW5 (Due 26th Sept)

Homework 5
Maude Source You should use this to copy the “skeleton” Maude Module code.

HW6 (Due 3rd Oct)

Homework 6
Maude Source You should use this to copy the “skeleton” Maude Module code.

HW7 (Due 10th Oct)

Homework 7

HW8 (Due 17th Oct)

Homework 8
Maude Source You should use this to copy the “skeleton” Maude Module code.

HW9 (Due 24th Oct)

Homework 9
Q1 Maude Source You should use this to copy the “skeleton” Maude Module code.
Q2 Maude Source You should use this to copy the “skeleton” Maude Module code.
Q2 Maude Script You should use this to copy the provided proof script.

HW10 (Due 31st Oct)

Homework 10
Q1 Maude Source You should use this to copy the “skeleton” Maude Module code.
Q1 Extra Credit Maude Source You should use this to copy the “skeleton” Maude Module code.
Q2 Maude Source You should use this to copy the “skeleton” Maude Module code.

HW11 (Due 7th Nov)

Homework 11
Q2 Maude Source You should use this to copy the “skeleton” Maude Module code.

HW12 (Due 14th Nov)

Homework 12
Q1 Maude Source You should use this to copy the “skeleton” Maude Module code.
Q2 Maude Source You should use this to copy the “skeleton” Maude Module code.

HW13 (Due 28th Nov)

Homework 13
Q2 Maude Source You should use this to copy the “skeleton” Maude Module code.
Q2 Extra Credit Maude Source You should use this to copy the “skeleton” Maude Module code.

Comprehensive Homework (Due 14th Dec)

Comprehensive Homework - Please read all of the important notes at the beginning
Q2 Maude Source - You should use this to copy the “skeleton” Maude Module code.
Q3 Maude Source - You should use this to copy the “skeleton” Maude Module code.
Q4 Maude Source - You should use this to copy the “skeleton” Maude Module code.

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 MscOS
$ 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, 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