CS476 Program Verification

Fall 2006

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

Place: 1103 Siebel Center

Office Hours: after class

News

Final Updated

The final has been updated with some clarifications on Problem 2, and the JavaFAN and JavaRL software used in problems 5 and 6.

Final Posted

The final has been posted. The main files you will need to download are listed here:

The final will require using the tools you have used before, including the Maude Inductive Theorem Prover, Sufficient Completeness Checker, and Maude Termination Tool. Additionally, the final will require using JavaRL which can be downloaded from http://fsl.cs.uiuc.edu/index.php/Rewriting_Logic_Semantics_of_Java. An introduction to JavaRL can be found in the lecture notes for 12/07.

The final also requires the new Maude coherence checker and confluence checker. In order to use this tool, you will need to latest Maude version 2.3 alpha. We include all of the files you will need below. This Maude executable is compiled for Linux and has been verified to run on the CSIL Linux core machines. You will need to download and unpack the archive below for Maude 2.3 along with the files for Full Maude and the Church-Rosser Checker.

Overview

Examines formal methods for demonstrating correctness and other properties of programs; includes an overview of predicate calculus. Topics include: invariant assertions, Hoare axiomatics, well-founded orderings for proving termination, structural induction, computational induction, data structures, and parallel programs.

Requirements

Participation
Readings and automated deduction experiments
Homeworks
Take-home final exam
For 1 unit, project or paper to be arranged with instructor

Texts

Latest draft of Maude book (Requires password from professor to access)
The Maude 2.2 Manual
Formal Modeling and Analysis of Distributed Systems in Maude

Software

All of the software used in this course is based on Maude, a reflective programming language based on term rewriting. In addition to Maude itself, we will use several tools written in Maude. Most of these tools are written to use the latest release of Maude — version 2.2. However, the Maude Inductive Theorem Prover requires Maude version 2.1.1. In order to make things simpler for students, all of the software used in this course is installed on the CSIL Linux machines. If you prefer, you can also download and install the software on a PC.

Maude

Maude 2.2: On CSIL machines at /home/class/fa06/cs476/bin/maude and also available for download.
Maude 2.1.1: On CSIL machines at /home/class/fa06/cs476/bin/maude-2.1.1 and also available for download.

Related Software

Maude Termination Tool (MTT)

Installed on the CSIL machines with instructions available from here.

Maude Church-Rosser Checker

Download from website and run using Maude 2.2

Maude Sufficient Completeness Checker

This tool requires a special version of Maude with extensions to the CETA library. The version of Maude installed on the CSIL machines already has these extensions. Otherwise, you must download the executable from the website. Once you have the proper Maude version, download scc.maude, and load it from the Maude prompt. See the tool website for more detailed instructions. Note that the SCC tool uses core Maude modules — not full-maude modules. You need to remove the parenthesis around Maude modules before loading them.

Maude ITP

The Maude Inductive Theorem Prover (ITP) can be used to prove theorems mechanically about Maude functional programming modules. Maude ITP requires Maude 2.1.1. Assuming you already have Maude 2.1.1, using Maude ITP requires the following steps:

Download the sources and documentation from this archive
Untar the files, e.g. tar xvfz itp-uiuc.tgz
Change to the ITP directory itp-uiuc/itp-files, and copy the module you wish to reason about to itp-uiuc/itp-files as well. For example, if you are proving theorems about list.itp, copy it into itp-uiuc/itp-files.
Start Maude 2.1.1; On the CSIL machines this is accomplished by running /home/class/fa06/cs476/bin/maude-2.1.1.
Load the Maude ITP by typing load itp-tool.
Load the module you wish to reason about using the Maude load or in commands. You should see the module name(s) printed out as they are loading.
If the module you loaded did not automatically start ITP and provide the goal, you need to start ITP with the Maude commands:
```
    Maude> select ITP-TOOL .
    Maude> loop init-itp .
  
```
If everything is working correctly, ITP should print out the message "ITP tool (March 7th, 2005)". For further documentation on how to use ITP, see the file itp-uiuc/itp-documentation.pdf in the itp-uiuc.tgz archive.

Maude Java+ITP

Download the sources and documentation from this archive. Java+ITP also requires Maude 2.1.1 and can be started by following the directions for ITP above.

Lecture Notes

No Date Last Updated Slides

1 08/24/08 08/25/06 lec01_aug_24.pdf

08/29/08

09/23/06

lec02_aug_29.pdf

`2.1.jpg`	`2.4.jpg`
`2.2.jpg`	`2.5.jpg`
`2.3.jpg`

3 08/31/08 10/26/06 lec03_aug_31.pdf

09/05/08

10/20/06

lec04_sep_05.pdf

4.1.jpg

5 09/07/08 09/06/06 lec05_sep_07.pdf

6 09/12/08 09/14/06 lec06_sep_12.pdf

7 09/14/08 09/14/06 lec07_sep_14.pdf

8 09/19/08 10/03/06 lec08_sep_19.pdf

09/21/08

09/21/06

lec09_sep_21.pdf

9.1.jpg

09/26/08

12/10/06

lec10_sep_26.pdf

10.1.jpg

11 09/28/08 09/24/06 lec11_sep_28.pdf

12 10/03/08 09/24/06 lec12_oct_03.pdf

13 10/05/08 09/24/06 lec13_oct_05.pdf

14 10/10/08 09/24/06 lec14_oct_10.pdf

15 10/12/08 09/24/06 lec15_oct_12.pdf

16 10/17/08 09/24/06 lec16_oct_17.pdf

17 10/19/08 10/20/06 lec17_oct_19.pdf

18 10/24/08 09/24/06 lec18_oct_24.pdf

19 10/26/08 10/22/06 lec19_oct_26.pdf

20 10/31/08 10/22/06 lec20_oct_31.pdf

21 11/02/08 11/02/06 lec21_nov_02.pdf

22 11/07/08 11/07/06 lec22_nov_07.pdf

23 11/09/08 11/07/06 lec23_nov_09.pdf

24 11/14/08 11/07/06 lec24_nov_14.pdf

25 11/16/08 11/07/06 lec25_nov_16.pdf

26 11/21/08
11/23/06 12/09/06 lec26_nov_21.pdf

27 11/30/08 12/09/06 lec27_nov_30.pdf

28 12/05/08 12/06/06 lec28_dec_05.pdf

29 12/07/08 12/07/06 lec29_dec_7.ppt

Homework Policy

All the assignments should be solved by each student individually. Although it is of course allowable to discuss contents of the course among students, such discussions should not include approaches to solve homework problems. Any such collaboration in homework would constitute a violation of the university's academic integrity.