Assigned work: Exercises 4.6 page 250-251 While loops #1 
	Hint: the invariant is x=y+a.

Weds Mar 12

1
 Chien-min Wang
 Binary Decision Diagrams and Beyond; enabling technologies for Formal Verification
 Randal E Bryant
 Proc. Int Conf CAD IEEE 1995 pp236-243
 
2
 James Warshawsky
 A Realistic Involvement of formal methods
 Didier Begay, Antoine Rauzy
 Software - P&E 2001
 
3
 Meng-Hsi Tsai
 Model Checking Software Architecture Specifications in Sam
 Xudong He, Junhua DIng, Yi Deng
 Proc 14th ICSE pp271-274 June 2002
 
4
 Chun-Kai Chiu
 The Model Checker Spin
 Gerard J Holzmann
 IEEE Trans SE-23n5 may 1997
 
5
 Bill Rutherford
 Model Exploration with Temporal Logic Query Checking
 Arie Gurfinkel, BEne Devereux, Marsha Checkik
 ACM SIGSOFT FSE-10 Nov 2002
 

Lab:  Presentations ran on into lab time and all present earned
	credit.

	No work assigned. 

Next:
http://www.csci.csusb.edu/dick/cs656/class/20.html