CS477 Formal Software Development Methods

Computer Science 477

Spring 2006

The final has been posted.

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

Place: 1103 Siebel Center

Instuctor: Jose Meseguer

Office Hours: after class

Course Topics

  1. Introduction
  2. Equational Logic
  3. Functional Programming in Equational Logic using Maude
  4. Verification of Functional Programs by Induction
  5. Algebraic Semantics of Imperative Programs
  6. Pre- and Post-conditions
  7. Invariants
  8. Termination
  9. Rewriting Logic Semantics of Concurrent Programs
  10. Verification of Concurrent 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

Software

Maude
On CSIL machines at /usr/dcs/csil/bin/maude and also available for download.
Full Maude
Available for download.
Maude ITP
Sources and documentation available for download. Note that this version of ITP requires Maude 2.1.1 located here.
Maude Termination Tool (MTT)
Installed on the CSIL machines with instructions available from here.
Maude Church-Rosser Checker
Installed on the CSIL machines — type /home/class/cs477/bin/crc to run.
Maude Sufficient Completeness Checker
Downloadable from tool website

Lecture Notes

No Date Slides Last Updated
2 01/19/2008 lec02_jan_19.pdf 01/20/2006
3 01/24/2008 lec03_jan_24.pdf 01/23/2006
4 01/26/2008 lec04_jan_26.pdf 02/02/2006
5 02/07/2008 lec05_feb_07.pdf 02/08/2006
6 02/14/2008 lec06_feb_14.pdf 02/16/2006
7 02/16/2008 lec07_feb_16.pdf 02/16/2006
8 02/21/2008 lec08_feb_21.pdf 02/20/2006
9 02/23/2008 lec09_feb_23.pdf 02/27/2006
10 02/28/2008 lec10_feb_28.pdf 03/02/2006
11 03/07/2008 lec11_mar_07.pdf 03/01/2006
12 03/09/2008 lec12_mar_09.pdf 03/01/2006
13 03/14/2008 lec13_mar_14.pdf 03/01/2006
14 03/16/2008 lec14_mar_16.pdf 03/01/2006
15 03/28/2008 lec15_mar_28.pdf 03/01/2006
16 03/30/2008 lec16_mar_30.pdf 03/07/2006
17 04/04/2008 lec17_apr_04.pdf 03/07/2006
18 04/06/2008 lec18_apr_06.pdf 03/07/2006
19 04/11/2008 lec19_apr_11.pdf 04/05/2006
20 04/13/2008 lec20_apr_13.pdf 04/13/2006
21 04/18/2008 lec21_apr_18.pdf 04/13/2006
22 04/20/2008 lec22_apr_20.pdf 04/13/2006
23 04/25/2008 lec23_apr_25.pdf 04/13/2006
24 04/27/2008 lec24_apr_27.pdf 04/13/2006
25 05/02/2008 lec25_may_02.pdf 04/13/2006

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.

Homeworks

No Given Due Homework
1 Jan. 19 Feb. 2 Homework #1
2 Feb. 14 Feb. 28 Homework #2
nat-mset-min.maude
3 Feb. 28 Mar. 14 Homework #3
ack.maude list1.maude
list.maude
4 Mar. 14 Mar. 30 Homework #4
list-hw4.maude list-itp.maude
goal.maude
5 Apr. 10 Apr. 20 Homework #5
This homework requires using two different versions of Maude ITP running under Maude 2.1.1 Exercise 3 requires the version of ITP used in homework 4 available here. Exercise 4 and 5 require the Java enhanced version of ITP available here. Additional files include:
card.maude insert-sort.maude
insert-sort.itp

For Homework #3, please see the documentation for using the Maude Termination Tool.

For homeworks 4 and 5, please download the appropriate version of Maude 2.1.1 for your platform along with ITP from the links in the Software section. For example, if you are using an Intel x86 machine, use need this version of Maude 2.1.1.

Final

The final is due at noon on Wednesday, May 10. You will need the following files: