Re: PVS Course Materials

[Mark Lawford <lawford@mcmaster.ca>]

Hi Sylvan.

For the past 3 of years I have been teaching a 2nd year
undergraduate course in our Software Engineering program titled: 

	SFWR ENG 2F04: Applications of Mathematical Logic in Software
			Engineering

as well as a graduate course titled:

	CS 734: Formal Methods for Real-Time Systems

Both make extensive use of PVS.  There are PDF and postscript versions of
my lecture slides, assignments, midterms, exams and some solutions and PVS
dump files available on the web from my home page:

	http://www.cas.mcmaster.ca/~lawford

The material on the web needs to be reorganized to make it easier to
navigate so if you are having trouble finding things, please contact me. 

The material includes introductory mathematical logic material and slides
to help the students understand PVS in terms of Natural Deduction proof
rules.  There are also several nice examples in the slides and assignments
of the use of PVS support for tabular methods to debug software
requirements specifications and to formally verify implementations. 

LaTeX versions of most of the above materials can be provided to
interested people upon request.  I only ask that anyone who uses the
materials and examples please credits me as the source and maintains my
copyright notice.  

I'd also appreciate it if people could provide suggestions for
improvements to the material and point out my mistakes.

Regards,
Mark Lawford

Dr. Mark Lawford
Assistant Professor                        Email: lawford@McMaster.ca
DEPARTMENT OF COMPUTING AND SOFTWARE       Tel: 905 525 9140 Ext. 24911
Faculty of Engineering                     Fax: 905 524 0340
McMaster University,                       Office: JHE 302/C
Hamilton, Ontario  Canada L8S 4K1          http://www.cas.mcmaster.ca/~lawford



On Wed, 21 Nov 2001, Sylvan S. Pinsky wrote:

> To All,
> 
> In a few weeks, I will be teaching a course in PVS for employees at our 
> Agency.  As I am preparing the course material, I have looked at the PVS
> home page, where there are some helpful briefings such as Shankar's CISM
> Lecture Notes.  I have also reviewed the link from Cambridge University to 
> the Educational Resources Page at Indiana University.
>  
>      http://www.cs.indiana.edu/formal-methods-education/
> 
> Does anyone have PVS materials that could be useful for teaching  PVS?  
> I think it would be beneficial to the PVS community to share information that 
> could contribute to the education and training of new users.  I will be happy 
> to make my material available after it has been developed and tested.
> 
> Regards,
> 
> Sylvan Pinsky
>