CS476 Program Verification

Fall 2007

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

Place: 1103 Siebel Center

Professor: José Meseguer

Office Hours: after class

News

Dec 10: Final Exam Questions

In problem 1, it is helpful to comment out the Multiset sort and the operations involving it. This should avoid many of the spurious errors generated by the ITP. In problem 4, the sorts State and Nat conflict with the model checker sorts with the same name. Those sorts may be renamed as needed to avoid syntax errors. Finally, in problem 6, the if statement without a body in the Listener class causes a parser error. This error may be fixed by adding an extra {} after the if statement. Thanks to Robert Blake for identifying these errors.

Dec 9: Updates

The JavaFAN slides have been updated. You may download the latest version from the lecture notes at the bottom of the page. Additionally, on the ITP exercises, Maude may print out many advisories. These are harmless, and can safely be ignored. If you want, you can disable them, by typing the command “set show advisories off .” before running ITP commands.

Dec 7: Final Posted

The final is now available, and is due at 5pm on Tuesday, Dec. 11. The final will require using the Maude Inductive Theorem Prover — both the original one, and the version from homework 6 with support for Java. 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/04. The files for the final are listed below:

• final.pdf
• insert-sort.maude
• insert-sort.itp
• maxnml.maude
• maxnml.itp
• unordered-channel.maude
• unordered-states.maude
• threadgame.java
• pipeline.java

Dec 5: Javafan Examples

Nov 13: Homework 6 Updated

The theoretical exercises in homework 6 have been updated a second time in the download below. Please download the homework again to get the updates.

Nov 11: Homework 6 Updated

The theoretical exercises in homework 6 have been updated in the download below. Please download the homework again to get the updates.

Nov 6: Homework 6

Download as PDF. Due on Nov. 27th. Exercise 4 requires the Maude ITP as used in previous homeworks while exercises 5 and 6 require a special version of the ITP that understands the Java semantics. This version of the ITP requires Maude 2.1.1, which is available for download from here and also installed on the CSIL machines at /home/class/fa07/cs476/bin/maude-2.1.1. In addition, you should download the ITP archive cs476_hw6.tar.gz available below along with the Maude modules for exercise 4:

• cs476_hw6.tar.gz
• nat.maude

Oct 21: Homework 5 Posted and ITP Updated

Download as PDF. Due on Nov. 6th. You should download the most recent version of the ITP before doing the exercises in this homework. The homework references the following modules and ITP goals:

• card.maude
• card.itp
• tree.maude
• sort.maude
• sort.itp

Oct 9: Homework 4 Posted

Download as PDF. Due on Oct. 23rd. The homework references the following module and ITP goal:

• itp-list.maude
• rev-append.itp

Oct 8: scc.maude updated

The version of the Maude SCC on the course webpage has been updated from an obsolete older version. If you encounter errors when running the SCC, you should redownload the latest version.

Oct 5: Maude SCC updated

The version of Maude used for sufficient completeness checking has been updated. You may now run the SCC with Maude 2.3 using the command /home/class/fa07/cs476/bin/maude rather than /home/class/fa07/cs476/bin/maude-2.2. See the Maude SCC description for more details.

Sep. 25: Homework 3 Posted

Download as PDF. Due on Oct. 9. This homework references several Maude modules available below:

• ack.maude
• list.maude
• list1.maude

Sep. 6: Homework 2 Posted

Download as PDF. Due on Sep. 25.

Aug. 8: Homework 1 Posted

Download as PDF.

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

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

Texts

• All About Maude — A High-Performance Rewriting Framework
• The Maude 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. 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 2.3

on csil machines at /home/class/fa07/cs476/bin/maude and also available for download.

Full Maude 2.3b

Full Maude is required for other tools below. It is installed on csil machines at /home/class/fa07/cs476/lib/maude-2.3/full-maude.maude and also available for download. If it is placed in the same directory as the maude executable (as it is on the csil machines), then it may be loaded by typing “load full-maude” within Maude.

Maude Termination Tool (MTT)

Installed on the CSIL machines with instructions available from here.

Maude Church-Rosser Checker (CRC)

Requires Full Maude. It is installed on csil machines at /home/class/fa07/cs476/lib/maude-2.3/crchc2a.maude and also available for download. If it is placed in the same directory as the maude executable (as it is on the csil machines), then it may be loaded by typing “load crchc2a” within Maude after loading Full Maude.

Maude Coherence Checker (ChC)

Bundled with the Maude Church-Rosser checker, and may be loaded the same way.

Maude Sufficient Completeness Checker

This tool requires a special version of Maude 2.3 with extensions to the CETA library. These extensions are included in the version of Maude is installed on the CSIL machines at /home/class/fa07/cs476/bin/maude. Otherwise, you must download the executable from the website. Once you have the proper Maude version, download scc.maude. After installing this file into the same directory as the Maude executable, load the module you with to check, type “load scc” to load the scc, and type “(scc ModuleName .)” to check the module with the given name . 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 Inductive Theorem Prover (course version)

This tool can be used to prove inductive theorems about a equational specification. The version on the tool's website is different than the one used for this course which is listed below. Documentation is available in the course lecture notes for lecture 12 and in a Adobe pdf including in the download. The examples for lecture 12 are also available in the archive. The ITP should be used with Maude 2.3 or a more recent version.

• itp-uiuc.tgz

Rewriting Logic Semantics of Java : JavaRL

Please see homepage for more details.

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.

Lecture Notes