CS476 Program Verification

Spring 2021

Time: Tuesday and Thursday, 9:30-10:45

Place: online course

Zoom Links:

Tuesday Lectures: https://illinois.zoom.us/j/84395222460?pwd=WHA4NUM5UzN3UXFMVGxZSWJVbk5jdz09

Thursday Lectures: https://illinois.zoom.us/j/84021076116?pwd=b1E2TTlnUEkxWmhnN1hlMkx1Zm5LQT09

Professor: Jose Meseguer

Staff: Reed Oei

Queries on course-related matters, as well as homework assignments, should be sent to Reed Oei at: reedoei2@illinois.edu

Office Hours: Immediately following class in the same Zoom session; and by appointment when needed.

Official Description

Formal methods for demonstrating correctness and other properties of programs. Invariant assertions; Hoare axiomatics; well-founded orderings for proving termination; structural induction; computational induction; data structures; parallel programs; overview of predicate calculus. Course Information: 3 undergraduate hours. 3 or 4 graduate hours. Prerequisite: CS 225; CS 374 or MATH 414.

Subject Area

Programming Languages / Formal Methods

Topics List

  • Algebraic specification of declarative sequantial programs
  • Inductive first-order logic and inductive theorem proving
  • Formal verification of declarative functional programs
  • Algebraic semantics of imperative sequential languages
  • Rewriting logic specification of declarative concurrent programs
  • Temporal logic and model checking verification of declarative concurrent programs
  • Rewriting logic semantics of imperative programs
  • Model checking verification of imperative concurrent programs
  • Hoare and Reachability logic verification of imperative programs

Learning Goals

  • Be able to model software systems mathematically using mathematical logic.
  • Be able to model mathematically the semantics of programs and to use such a semantics to verify program properties.
  • Be able to fornally verify both sequential and concurrent programs in both declarative and imperative languages.
  • Be able to to develop correct formal executable specifications of software systems, and to use such specifications to verify system properties.
  • Be able to correctly use the main logics involved in the verification of both sequential and concurrent programs and systems, including, equational logic, rewriting logic, inductive first-order loic, Hoare logic, and temporal logic.
  • Be able to effectively and competently use formal verification tools such as formal specification languages, theorem provers, and model checkers to verify programs and systems using all the above-mentioned logics in non-trivial practical examples.
 

Reading Materials


Comprehensive Homework (due: May 11)


Course Work, Policies and Procedures

Students taking the course will be expected to:

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.

Homework

Homework 1 (due: Feb 2)

PDF LaTeX

Homework 2 (due: Feb 9)

PDF

Homework 3 (due: Feb 16)

PDF, LaTeX, Maude module

Homework 4 (due: Feb 23)

PDF, LaTeX, Maude module

Homework 5 (due: Mar 02)

PDF, LaTeX, Maude module

Homework 6 (due: Mar 09)

PDF, LaTeX, Maude module

Homework 7 (due: Mar 16)

PDF, LaTeX, Maude module

Homework 8 (due: Mar 23)

PDF, LaTeX

Homework 9 (due: Mar 30)

PDF, LaTeX

Homework 10 (due: Apr 6)

PDF

LaTex

Homework 11 (due: Apr 14)

PDF

Latex

Homework 12 (due: Apr 20)

PDF, LaTeX

Homework 13 (due: Apr 27)

PDF, LaTeX

Homework 14 (due: May 4)

PDF, LaTeX

Comprehensive Homework (due: May 11)

PDF

LaTex

 


Lectures

Lecture 01 - Jan 26, 2021

Lecture Slides

Lecture 02 - Jan 28 & Feb 2, 2021

Lecture Slides

Signature Diagrams: Diagram 1, Diagram 2, Diagram 3

Lecture 03 - Feb 4, 2021

Lecture Slides

Lecture 04 - Feb 9, 2021 & Feb 11, 2021

Lecture Slides, Diagram, Recording

Lecture 05 - Feb 16, 2021 & Feb 18, 2021

Lecture Slides

Lecture 06 - Feb 23, 2021 & Feb 25, 2021

Lecture Slides

Lecture 07 - Mar 3, 2021 & Mar 5, 2021

Lecture Slides

Lecture 08 - Mar 9, 2021 & Mar 11, 2021

Lecture Slides

Lecture 09 - Mar 16, 2021 & Mar 18, 2021

Lecture Slides

Lecture 10 - Mar 23, 2021 & Mar 25, 2021

Lecture Slides

Lecture 11 - Mar 30, 2021 & Apr 1, 2021

Lecture Slides

Lecture 12 - Apr 6, 2021 & Apr 8, 2021

Lecture Slides

Lecture 13 - Apr 8, 2021

Lecture Slides

Lecture 14 - Apr 15, 2021 & Apr 20, 2021

Lecture Slides

Lecture 15 - Apr 20, 2021 & Apr 22, 2021

Lecture Slides

Lecture 16 - Apr 27, 2021 & Apr 29, 2021

Lecture Slides

Lecture 17- Apr 29 & May 4, 2021

Lecture Slides

 


 

Maude

Maude will be the primary tool used in this course, but several tools/libraries written in Maude will also be used. Some of these libraries require extra functionality to be added directly to Maude (at the C++ level). You can choose to build from the Maude sources or directly from binary releases of Maude 2.7.1.

 
# Download and unzip Maude 2.7.1 binary release for Linux
$ wget 'https://github.com/maude-team/maude/releases/download/v2.7.1-ext-hooks/maude-2.7.1-linux.tar.gz'
$ tar -xvf maude-2.7.1-linux.tar.gz
# Run Maude
$ ./maude
 
# Download Maude 2.7.1 binary release for MacOS
$ wget 'http://maude.cs.illinois.edu/w/images/2/25/Maude-2.7.1-osx.zip'
$ unzip Maude-2.7.1-osx.zip
$ chmod +x ./maude.darwin64
# Run Maude
$ ./maude.darwin64
 
\||||||||||||||||||/
--- Welcome to Maude ---
/||||||||||||||||||\
Maude 2.7.1 built: Aug 31 2016 18:22:38
Copyright 1997-2016 SRI International
Sun Oct 1 11:59:31 2017
Maude>

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. Note that if you are using Maude 2.7.1, and not the latest version of Maude (currently the latest is 3.1), you should download this release. Otherwise, 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:

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

Maude Inductive Theorem Prover

Go to the Maude ITP Webpage to download the sources for the Maude ITP. The Maude ITP runs on Maude 2.7.

Commands that you may find useful (see the tutorial on the Maude ITP website):

Using the following example module:

fmod NATURAL-ORD is
  sort Natural .
  op 0 : -> Natural [ctor] .
  op s : Natural -> Natural [ctor] .
  op _<_ : Natural Natural -> Bool .
  op _=<_ : Natural Natural -> Bool .
  vars N M : Natural .
  eq N < 0 = false .
  eq 0 < s(N) = true .
  eq s(N) < s(M) = N < M .
  ceq N =< M = true if N < M .
  ceq N =< M = true if not(M < N) .
  ceq N =< M = false if M < N .
endfm

An example interaction to prove that this defines a linear order on natural numbers is:

 
# Download and unpack the Maude itp
$ wget 'http://maude.cs.uiuc.edu/tools/itp/maude_itp.tar.gz'
$ tar -xvf maude_itp.tar.gz
\||||||||||||||||||/
--- Welcome to Maude ---
/||||||||||||||||||\
Maude 2.7 built: Oct 17 2017 22:51:54
Copyright 1997-2014 SRI International
Tue Oct 17 23:40:31 2017
Maude> load maude_itp/itp-tool.maude
Maude> load nat-ord.maude
Maude> select ITP-TOOL .
Maude> loop init-itp .
Warning: sort declarations for operator _;_ failed preregularity check on 15 out of 2116 sort tuples. First such tuple is (AtomicTermSet, TermQid).
Warning: sort declarations for operator if_then_else_fi failed preregularity check on 12 out of 4232 sort tuples. First such tuple is (Bool, AtomicTermSet, TermQid).
Warning: sort declarations for associative operator _;_ are non-associative on 153 out of 97336 sort triples. First such triple is (TermSet, AtomicTermSet, TermQid).
--- You may encounter the warnings shown above; they should not affect you while using the ITP tool.
 
ITP tool (May 25th, 2006)
 
--- Introduce linearity goal
--- ------------------------
 
Maude> (goal linear : NATURAL-ORD |- A{N:Natural ; M:Natural} (((N =< M) or (M =< N)) = (true)) .)
rewrites: 1200 in 18ms cpu (18ms real) (66666 rewrites/second)
 
=================================
label-sel: linear@0
=================================
A{M:Natural ; N:Natural}
N:Natural =< M:Natural or M:Natural =< N:Natural = true
 
+++++++++++++++++++++++++++++++++
 
--- Use lemma of constants
--- ----------------------
 
Maude> (cns .)
rewrites: 223 in 3ms cpu (2ms real) (74333 rewrites/second)
New goals:
 
=================================
label-sel: linear@0
=================================
N*Natural =< M*Natural or M*Natural =< N*Natural = true
 
+++++++++++++++++++++++++++++++++
 
--- Split on N < M
--- --------------
 
Maude> (split on (N*Natural < M*Natural) .)
rewrites: 222 in 5ms cpu (5ms real) (44400 rewrites/second)
New goals:
 
=================================
label-sel: linear@1.0
=================================
N*Natural =< M*Natural or M*Natural =< N*Natural = true
 
=================================
label: linear@2.0
=================================
N*Natural =< M*Natural or M*Natural =< N*Natural = true
 
+++++++++++++++++++++++++++++++++
 
--- Discharge goal 1 with assumptions
--- ---------------------------------
 
Maude> (auto .)
rewrites: 112 in 0ms cpu (0ms real) (~ rewrites/second)
Eliminated current goal.
 
New current goal:
 
=================================
label-sel: linear@2.0
=================================
N*Natural =< M*Natural or M*Natural =< N*Natural = true
 
+++++++++++++++++++++++++++++++++
 
--- Discharge goal 2 with assumptions
--- ---------------------------------
 
Maude> (auto .)
rewrites: 54 in 0ms cpu (0ms real) (~ rewrites/second)
Eliminated current goal.
 
q.e.d
 
+++++++++++++++++++++++++++++++++

RLTool Command Overivew

Here is the command listing from rltool-lib.maude in the tool archive.

RLTool

sort @QFForm@ @QFCTerm@ @NeQFCTermSet@ @Term@ @TermSet@ @ReachFormEx@ @LabelReachFormEx@ .
subsort @QFCTerm@ < @NeQFCTermSet@ .
subsort @Term@ < @TermSet@ .
op ((_))     : @Bubble@                      -> @Term@ [ctor] .
op _U_       : @TermSet@ @TermSet@           -> @TermSet@ [assoc comm ctor] .
op true      :                               -> @QFForm@ [ctor] .
op (_)=(_)   : @Bubble@ @Bubble@             -> @QFForm@ [ctor] .
op (_)=/=(_) : @Bubble@ @Bubble@             -> @QFForm@ [ctor] .
op _/\_      : @QFForm@ @QFForm@             -> @QFForm@ [prec 58 assoc comm ctor] .
op _\/_      : @QFForm@ @QFForm@             -> @QFForm@ [prec 59 assoc comm ctor] .
op (_)|_     : @Bubble@ @QFForm@             -> @QFCTerm@ [prec 60 ctor] .
op _\/_      : @NeQFCTermSet@ @NeQFCTermSet@ -> @NeQFCTermSet@ [prec 61 assoc comm ctor] .
op _=>_      : @NeQFCTermSet@ @NeQFCTermSet@ -> @ReachFormEx@ [prec 62 ctor] .
op _:_       : @Token@ @ReachFormEx@         -> @LabelReachFormEx@ [prec 63 ctor] .

sort MetaRLTLCommand .
--- module/var/backend setup
op select_.               : @Token@ -> MetaRLTLCommand [ctor] .
op select-rls_.           : @NeTokenList@ -> MetaRLTLCommand [ctor] .
op declare-vars_.         : @TermSet@ -> MetaRLTLCommand [ctor] .
op use`tool_for_on_.      : @Token@ @Token@ @Token@ -> MetaRLTLCommand [ctor] .
op use`tool_for_on_with_. : @Token@ @Token@ @Token@ @NeTokenList@ -> MetaRLTLCommand [ctor] .

--- goal/term state setup
op def-term-set_.         : @NeQFCTermSet@ -> MetaRLTLCommand [ctor] .
op add-goal_.             : @LabelReachFormEx@ -> MetaRLTLCommand [ctor] . --- add as goal and axiom
op add-goal!_.            : @LabelReachFormEx@ -> MetaRLTLCommand [ctor] . --- add as goal
op add-axiom_.            : @LabelReachFormEx@ -> MetaRLTLCommand [ctor] . --- add as axiom TODO: revisit this command
op inv_to_with_on_.       : @Token@ Qid @TermSet@ @NeQFCTermSet@ -> MetaRLTLCommand [ctor] .
op inv_to_on_.            : @Token@ Qid @NeQFCTermSet@ -> MetaRLTLCommand [ctor] .

--- finish setup
op start-proof`.          : -> MetaRLTLCommand [ctor] .

--- proof manipulation
--- apply basic proof strategy
op auto_.                 : Nat -> MetaRLTLCommand [ctor] .
op auto*`.                : -> MetaRLTLCommand [ctor] .
op auto`.                 : -> MetaRLTLCommand [ctor] .
--- delete unwanted goals
op focus_.                : NeSet{Nat} -> MetaRLTLCommand [ctor] .
op focus_.                : @Term@ -> MetaRLTLCommand [ctor] .
op focus_.                : @QFCTerm@ -> MetaRLTLCommand [ctor] .
op focus_/_.              : @QFCTerm@ @QFCTerm@ -> MetaRLTLCommand [ctor] .
--- change axioms used
op use-axioms_on_.        : @NeTokenList@ Nat -> MetaRLTLCommand  [ctor] .               --- modify goal to use circularities
op use-axioms_._on_.      : @NeTokenList@ @NeTokenList@ Nat -> MetaRLTLCommand  [ctor] . --- modify goal to use axioms/circularities
--- do case analysis a variable
op case_on_by_.           : Nat @Token@ @TermSet@ -> MetaRLTLCommand [ctor] .
op case_on_by_.           : @Term@ @Token@ @TermSet@ -> MetaRLTLCommand [ctor] .
op case_on_by_.           : @QFCTerm@ @Token@ @TermSet@ -> MetaRLTLCommand [ctor] .
--- split on a formula
op split_by_.             : Nat @QFForm@ -> MetaRLTLCommand [ctor] .
op split_by_.             : @Term@ @QFForm@ -> MetaRLTLCommand [ctor] .
op split_by_.             : @QFCTerm@ @QFForm@ -> MetaRLTLCommand [ctor] .
op replace_by_.           : Nat @QFForm@ -> MetaRLTLCommand [ctor] .
op replace_by_.           : @Term@ @QFForm@ -> MetaRLTLCommand [ctor] .
op replace_by_.           : @QFCTerm@ @QFForm@ -> MetaRLTLCommand [ctor] .
op split_by_and_.         : Nat @QFForm@ @QFForm@ -> MetaRLTLCommand [ctor] .
op split_by_and_.         : @Term@ @QFForm@ @QFForm@ -> MetaRLTLCommand [ctor] .
op split_by_and_.         : @QFCTerm@ @QFForm@ @QFForm@ -> MetaRLTLCommand [ctor] .
--- try to close a set of goals with default strategy---but do nothing if this process fails
op try-finish_.           : NeSet{Nat} -> MetaRLTLCommand [ctor] .
op try-finish_.           : @QFCTerm@ -> MetaRLTLCommand [ctor] .
op try-finish_/_.         : @QFCTerm@ @QFCTerm@ -> MetaRLTLCommand [ctor] .
--- try to subsume a goal by another
op subsume_by_.           : Nat Nat -> MetaRLTLCommand [ctor] .
--- resume from a debugging output pause
op continue`.             : -> MetaRLTLCommand [ctor] .
--- delete inactive goals
op delete-inactive`.      : -> MetaRLTLCommand [ctor] .

--- output commands
op show-goal-table`.           : -> MetaRLTLCommand [ctor] .
op show-goal-ids`.             : -> MetaRLTLCommand [ctor] .
op show-all-goal-ids`.         : -> MetaRLTLCommand [ctor] .
op show-goals_.                : NeSet{Nat} -> MetaRLTLCommand [ctor] .
op show-goals`.                : -> MetaRLTLCommand [ctor] .
op show-level_.                : Nat -> MetaRLTLCommand [ctor] .
op show-levels`.               : -> MetaRLTLCommand [ctor] .
op show-ancestors_generation_. : NeSet{Nat} Bound -> MetaRLTLCommand [ctor] .
op show-narrowings_.           : Nat -> MetaRLTLCommand [ctor] .
op show-maude-cmd_on_.         : @Token@ Nat -> MetaRLTLCommand [ctor] .