References

CS734 Course Material

• A detailed course outline is available in HTML format. It has links to the relevant lecture slides.
• Course handouts, examples, lecture slides etc. are in the Notes directory.
• Part of the course material is based upon a few of my recent publications:

  M. Lawford, J. McDougall, P. Froebel and G. Moum ``Practical application of functional and relational methods for the specification and verification of safety critical software,'' In T. Rus, editor, Proceedings of Algebraic Methodology and Software Technology, 8th International Conference, AMAST 2000, LNCS 1816, Springer, Iowa City, Iowa, USA, May 2000, pp. 7--88.

  M. Lawford and H. Wu, ``Verification of Real-Time Control Software Using PVS,'' In P. Ramadge and S. Verdu, eds., Proceedings of the 2000 Conference on Information Sciences and Systems, vol. 2, Dept. of Electrical Engineering, Princeton University, Princeton, NJ, pp. TP1-13--TP1-17, 2000.

Introductory Logic References

• If you haven't had a course in mathematical logic before such as the 2nd year undergraduate software engineering SFWR ENG 2F04: Applications of Mathematical Logic for Software Engineers, then you might want to go to the 2F04 Homepage first.
• Introductory Texts:

  1.  Jean E. Rubin, Mathematical Logic: Applications and Theory, Saunders College Publishing, 1990.

  2.   W. K. Grassmann and Jean-Paul Tremblay, Logic and Discrete Mathematics: A Computer Science Perspective, Prentice-Hall, 1996.

  3.   Michael R. A. Huth and Mark D. Ryan, Logic in Computer Science: Modeling and Reasoning about Systems, Cambridge University Press, 2000.

More PVS Material

For more information on PVS, please consult the following documents:

• PVS Manuals (System Guide, Language Reference, Prover Guide and so on)
• A Tutorial Introduction to PVS
• A Less Elementary Tutorial
• An SRI Report Analyzing Tabular and State-Transition Requirements Specifications in PVS
• Another SRI Report Subtypes for Specifications: Predicate Subtypes in PVS