Formal MethodsEducational Resources

Formal Methods Education Resources

Course Pages

Main Page | Courses | Examples | Readings | Position Papers | Instructional Materials | Tools | Jobs | Submit

---

Introductory Computer Science Courses | Hardware Verification Courses | Software Verification CoursesSoftware Modeling Courses | Software Engineering Courses | Logic Courses | Other Courses

Introductory Computer Science Courses

• Foundations of Computer Science

  Level and Type	Undergraduate ; Lecture
  Developed By	Lawrence C Paulson
  Offered At	University of Cambridge ; Department of Computer Science
  Text Used	Paulson, ML for the Working Programmer
  Materials Offered	Examples, Lecture Notes
  Notes	The course teaches programming to beginners using Standard ML. Algorithmic ideas such as O-notation are covered too, as is data abstraction. The concepts covered include list processing, trees, exception handling, lazy lists and imperative data structures (mutable lists).

• Principles of Computing and Programming

  Level and Type	Undergraduate ; Laboratory, Lecture
  Developed By	Matthias Felleisen, Corky Cartwright, and others
  Offered At	Rice University ; Department of Computer Science
  Tools Used	DrScheme
  Text Used	How to Design Programs, by Felleisen, Findler, Flatt, and Krishnamurthi
  Materials Offered	Assignments, Handouts, Lecture Notes, programming environment (DrScheme)

• Formal Fault Verification

  Level and Type	Undergraduate, M.Tech , Pre - Ph.D. ; Seminar, Laboratory, Lecture, Recent Research Papers
  Developed By	Dr Aarti Gupta
  Offered At	Indian Institute of Technology Delhi India ; Department of Electrical/Computer Engineering, Department of Computer Science
  Tools Used	VIS, SMV
  Materials Offered	Projects, Examples, Assignments, Handouts, Lecture Notes

• Foundations of Computer Science

  Level and Type	Undergraduate ; Lecture
  Developed By	Peter Henderson
  Offered At	SUNY at Stony Brook ; Department of Computer Science
  Materials Offered	Assignments, Lecture Notes

• Discrete Mathematics

  Level and Type	Undergraduate ; Lecture
  Developed By	Rex Page
  Offered At	University of Oklahoma ; Department of Computer Science
  Tools Used	Propositional Proof Checker
  Text Used	Hall, O'Donnell, Discrete Mathematics Using a Computers
  Materials Offered	Projects, Examples, Assignments, Handouts, Lecture Notes, Solutions, Examinations
  Notes	Topics include logic, relations, functions, trees, graphs, and computational complexity. Emphasizes reasoning about software.

Hardware Verification Courses

• Verification of Digital Systems

  Level and Type	Lecture
  Developed By	Adnan Aziz
  Offered At	University of Texas at Austin ; Department of Electrical/Computer Engineering
  Tools Used	VIS
  Materials Offered	Projects, Assignments, Lecture Notes, Readings

• Formal Specification and Verification of Hardware

  Level and Type	Lecture
  Developed By	Shiu-Kai Chin
  Offered At	Syracuse University ; Department of Electrical/Computer Engineering, Department of Computer Science
  Tools Used	HOL
  Materials Offered	Assignments

• Applied Computer-Aided Verifcation

  Level and Type	Graduate, Undergraduate ; Seminar, Lecture
  Developed By	Kathi Fisler
  Offered At	Rice University ; Department of Computer Science
  Tools Used	SMV, PVS
  Materials Offered	Projects, Assignments, Handouts

• Formal Methods for System Design

  Developed By	Ganesh Gopalakrishnan
  Offered At	University of Utah ; Department of Computer Science
  Tools Used	Spin
  Materials Offered	Lecture Notes

• Specification and Verification I

  Level and Type	Lecture
  Developed By	Mike Gordon
  Offered At	University of Cambridge Computer Laboratory ; Department of Computer Science
  Materials Offered	Lecture Notes, Readings

• Specification and Verification II

  Level and Type	Lecture
  Developed By	Mike Gordon
  Offered At	University of Cambridge Computer Laboratory ; Department of Computer Science
  Materials Offered	Lecture Notes, Readings

• Automatic Formal Verification

  Level and Type	Graduate ; Seminar, Lecture
  Developed By	Alan Hu
  Offered At	University of British Columbia ; Department of Computer Science
  Tools Used	Murphi
  Materials Offered	Assignments, Readings

• Verification of Mixed Hardware-Software Systems

  Level and Type	Graduate ; Lecture
  Developed By	Alan Hu
  Offered At	University of British Columbia ; Department of Computer Science
  Tools Used	Murphi
  Materials Offered	Projects, Readings

• Using HOL: A Primer

  Level and Type	Graduate, Undergraduate ; self paced tutorial
  Developed By	Phillip J. Windley
  Offered At	Brigham Young University ; Department of Computer Science
  Tools Used	HOL
  Materials Offered	Projects, Examples, Assignments, Lecture Notes
  Notes	This self-paced tutorial is used in several courses I teach. It is not a course in its own right. Thye empahsis is on hardware verification. There are several more lessons forthcoming. The goal is to teach skills sufficient to verify a simple microprocessor.

• Hardware Formal Verification

  Level and Type	Graduate ; Lecture
  Developed By	Sofične Tahar
  Offered At	Concordia University ; Department of Electrical/Computer Engineering
  Materials Offered	Projects

• Computer-Aided Verification

  Level and Type	Lecture
  Developed By	Tom Henzinger
  Offered At	University of California at Berkeley ; Department of Electrical/Computer Engineering, Department of Computer Science
  Tools Used	MOCHA
  Text Used	Computer-Aided Verification: An Introduction to Model Building and Model Checking for Concurrent Systems

• Seminar on Embedded Systems

  Level and Type	Graduate ; Seminar
  Developed By	Rajeev Alur
  Offered At	University of Pennsylvania ; Department of Computer Science
  Materials Offered	Handouts

• Computer-Aided Verification

  Level and Type	Graduate, Undergraduate ; Lecture
  Developed By	Rajeev Alur
  Offered At	University of Pennsylvania ; Department of Computer Science
  Tools Used	Spin, SMV
  Text Used	Computer-aided verification by Alur and Henzinger
  Materials Offered	Lecture Notes

• Dependable Systems Case Study

  Level and Type	Graduate ; Laboratory, Lecture
  Developed By	Scott Hazelhurst
  Offered At	University of the Witwatersrand, Johannesburg ; Department of Computer Science
  Tools Used	PVS, Voss
  Text Used	Thomas Kropf. Formal Hardware Verification: Methods and Systems in Comparison. LNCS1287

• Mechanical Verification

  Level and Type	Undergraduate ; Laboratory, Lecture
  Developed By	Jim Grundy
  Offered At	The Australian National University ; Department of Computer Science
  Tools Used	HOL
  Materials Offered	Assignments, Lecture Notes, laboratory exercises

• Verification of reactive systems

  Level and Type	Graduate ; Lecture
  Developed By	Henny Sipma, Zohar Manna
  Offered At	Stanford University ; Department of Computer Science
  Tools Used	STeP
  Text Used	Lecture Notes
  Materials Offered	Articles and links to relevant sites
  Notes	People interested in the handwritten notes that are handed out in class can contact Henny Sipma at sipma@cs.stanford.edu to obtain a paper copy.

• Formal Fault Verification

  Level and Type	Undergraduate, M.Tech , Pre - Ph.D. ; Seminar, Laboratory, Lecture, Recent Research Papers
  Developed By	Dr Aarti Gupta
  Offered At	Indian Institute of Technology Delhi India ; Department of Electrical/Computer Engineering, Department of Computer Science
  Tools Used	VIS, SMV
  Materials Offered	Projects, Examples, Assignments, Handouts, Lecture Notes

• Introduction to Verification

  Level and Type	Undergraduate ; Lecture
  Developed By	Steven D. Johnson
  Offered At	Indiana Univerisity ; Department of Computer Science
  Tools Used	SMV, PVS
  Materials Offered	Projects, Assignments, Handouts, Readings
  Notes	Emphasis on exposure to tools with mathematical foundations as the need arises. A work in progress

• Formal Verification - A Tutorial

  Level and Type	Tutorial
  Developed By	Hans Eveking
  Offered At	Darmstadt University of Technology, Germany ; Department of Electrical/Computer Engineering, Tutorial (3-4 h) given at DATE'98, DATE'99 and at Linköping Univ.
  Materials Offered	Handouts
  Notes	There is also a zipped pdf version available at our research home-page http://www.rs.e-technik.tu-darmstadt.de/TUD/res/res.html

• Automatic Verification

  Level and Type	Graduate ; Lecture
  Developed By	Marsha Chechik
  Offered At	University of Toronto ; Department of Computer Science
  Tools Used	Spin, SMV, PVS, Concurrency Workbench, Larch, COSPAN, TLA, Z
  Materials Offered	Assignments, Handouts, Lecture Notes

Software Verification Courses

• Software Validation and Verification

  Level and Type	Lecture
  Developed By	Karen Bernstein
  Offered At	DePaul University ; Department of Computer Science
  Tools Used	Spin
  Materials Offered	Assignments, Handouts

• Verification of Mixed Hardware-Software Systems

  Level and Type	Graduate ; Lecture
  Developed By	Alan Hu
  Offered At	University of British Columbia ; Department of Computer Science
  Tools Used	Murphi
  Materials Offered	Projects, Readings

• Ingenieria de Software

  Level and Type	Undergraduate ; Lecture
  Developed By	Maximiliano Cristia
  Offered At	Facultad de Ciencias Exactas, Ingenieria y Agrimensura - Universidad Nacional de Rosario - Argentina ; Department of Computer Science
  Text Used	Ghezzi, C., Jazayeri, M. y Mandrioli, D., Fundamentals of Software Engineering, Prentice Hall, Upper Saddle River, 1991
  Materials Offered	Examples, Assignments, Handouts, Lecture Notes
  Notes	The course and the Web page are held in Spanish.

• CMU 15-671: Models of Software Systems

  Level and Type	Graduate, Masters in Software Engineering ; Lecture
  Developed By	David Garlan
  Offered At	Carnegie Mellon University ; Department of Computer Science, Master in Software Engineering Program
  Materials Offered	Assignments, Handouts, Lecture Notes

• Mechanical Verification

  Level and Type	Undergraduate ; Laboratory, Lecture
  Developed By	Jim Grundy
  Offered At	The Australian National University ; Department of Computer Science
  Tools Used	HOL
  Materials Offered	Assignments, Lecture Notes, laboratory exercises

• Verification of reactive systems

  Level and Type	Graduate ; Lecture
  Developed By	Henny Sipma, Zohar Manna
  Offered At	Stanford University ; Department of Computer Science
  Tools Used	STeP
  Text Used	Lecture Notes
  Materials Offered	Articles and links to relevant sites
  Notes	People interested in the handwritten notes that are handed out in class can contact Henny Sipma at sipma@cs.stanford.edu to obtain a paper copy.

• Formal Fault Verification

  Level and Type	Undergraduate, M.Tech , Pre - Ph.D. ; Seminar, Laboratory, Lecture, Recent Research Papers
  Developed By	Dr Aarti Gupta
  Offered At	Indian Institute of Technology Delhi India ; Department of Electrical/Computer Engineering, Department of Computer Science
  Tools Used	VIS, SMV
  Materials Offered	Projects, Examples, Assignments, Handouts, Lecture Notes

• Introduction to Verification

  Level and Type	Undergraduate ; Lecture
  Developed By	Steven D. Johnson
  Offered At	Indiana Univerisity ; Department of Computer Science
  Tools Used	SMV, PVS
  Materials Offered	Projects, Assignments, Handouts, Readings
  Notes	Emphasis on exposure to tools with mathematical foundations as the need arises. A work in progress

• Formal Specification of Software (CSC227)

  Level and Type	Undergraduate ; Laboratory, Lecture
  Developed By	Steve Riddle
  Offered At	University of Newcastle upon Tyne, UK ; Department of Computer Science
  Tools Used	IFAD VDMTools & Toolbox Lite
  Text Used	John Fitzgerald and Peter Gorm Larsen, "Modelling Systems: Practical Tools and Techniques for Software Development", Cambridge University Press 1998, ISBN 0521 62348 0
  Materials Offered	Examples, Assignments, Handouts, Lecture Notes
  Notes	The course provides an introduction to modelling data and functionality using VDM-SL, a model-oriented specification language. The stress is on practical modelling skills rather than language detail. The examples and coursework exercises are based on industrial applications and the tools support understanding of specifications by admitting execution of formal models. Some discrete math and some functional programming have been found to be useful prerequisites.

• Applicative Programming and Specification

  Level and Type	Undergraduate ; Lecture
  Developed By	Don Sannella
  Offered At	University of Edinburgh ; Department of Computer Science
  Tools Used	Extended ML
  Materials Offered	Examples, Assignments, Handouts, exams
  Notes	This is a master's level course taken mainly by students with a first degree in something other than computer science. It covers: programming in SML (including modules), specification in Extended ML, and a little on correctness proofs.

• Logical Foundations of Programming

  Level and Type	Undergraduate ; Lecture
  Developed By	Michael Huth
  Offered At	Kansas State University ; Computing and Information Sciences
  Tools Used	SMV
  Text Used	M. Huth and M. Ryan; Logic in Computer Science: modelling and reasoning about systems; Cambridge University Press, 2000.
  Materials Offered	Examples, Assignments, Handouts
  Notes	The textbook is supported by a website which features an online, multiple-choice tutor, instructional material, and more. It can be found at http://www.cis.ksu.edu/~huth/lics/

• Automatic Verification

  Level and Type	Graduate ; Lecture
  Developed By	Marsha Chechik
  Offered At	University of Toronto ; Department of Computer Science
  Tools Used	Spin, SMV, PVS, Concurrency Workbench, Larch, COSPAN, TLA, Z
  Materials Offered	Assignments, Handouts, Lecture Notes

• Program Verification

  Level and Type	Undergraduate ; Lecture
  Developed By	Peter H. Roosen-Runge
  Offered At	York University ; Department of Computer Science
  Tools Used	suite of verification tools developed in Prolog (see text)
  Text Used	Software Verification Tools (unpublished)
  Materials Offered	Projects, Assignments, Handouts, Lecture Notes, text, _Software Verification Tools_, (PDF file)
  Notes	The focus of the course is the use of simple tools to support various aspects of software verification. The tools are: * wang -- uses method of sequents to check tautologies tautologies containing descriptive terms Applications: logic problems derived from English or mathematical statements. * simplify -- rewrite system used to implement arithmetic and abstract datatypes. Applications: verifying Forth and stack-based programs symbolic evaluation of functional expressions * prover -- combines simplify + wang + 'paramodulation' Applications: verifying identities on abstract datatypes; verifying implementation of one ADT by another. verification of refinement of Java interface specifications * induction -- uses prover to prove identities involving simple and tail-recursive functional expressions. * symbex -- uses wang and simplify to symbolically execute C/Java assignment and procedure statements, check assertions and generate post-conditions Applications: verifying straight-line assembler and loop-free C/Java code segments * wp -- derive Hoare-style pre-conditions from simple C/Java code: assignment, computations on array elements, conditionals, while-loops. Verify code segments annotated with invariant and variant specifications.

• Design and Analysis of Communication Software

  Level and Type	Graduate, Undergraduate ; Laboratory, Lecture
  Developed By	Patrice Godefroid in collaboration with David L. Dill
  Offered At	Stanford University ; Department of Electrical/Computer Engineering
  Tools Used	VeriSoft
  Materials Offered	Projects, Handouts

• Protocol Validation

  Level and Type	Undergraduate ; Lecture
  Developed By	Joost-Pieter Katoen
  Offered At	University of Twente ; Department of Computer Science
  Tools Used	Spin, Uppaal and NuSMV
  Text Used	Lecture notes and copies of papers
  Materials Offered	Assignments, Lecture Notes
  Notes	The course focuses on the automated verification of protocols using model checking with LTL, CTL and real-time CTL. The focus of the course is on obtaining experience with model checkers to treat small sized, non-trivial, problems.

• Systematic Software Development

  Level and Type	Graduate, Undergraduate ; Laboratory, Lecture, Term Project
  Developed By	Janusz Laski
  Offered At	Oakland Univeristy ; Computer Science and Engineering
  Tools Used	VDM-SL Toolbox
  Text Used	J.Fitzerald, P.Larsen, "Modelling Systems: Practical Tools and Techniques in Software Development."
  Materials Offered	Projects, Syllabus
  Notes	The page will be updated by providing concrete project examples.

• Protocol Validation

  Level and Type	Undergraduate ; Laboratory, Lecture
  Developed By	Frits Vaandrager
  Offered At	Faculty of Science, University of Nijmegen ; Department of Computer Science
  Tools Used	Murphi, Uppaal
  Text Used	Course notes, papers from the literature
  Materials Offered	Projects, Examples, Assignments, Handouts
  Notes	This course presents an overview of mathematical techniques for the specification and validation of reactive software systems. The techniques are illustrated using various distributed algorithms and comunication protocols. Topics that are addressed include I/O automata, invariant proofs, safety vs liveness, fairness, simulation relations, temporal logic, model checking, timed automata, hybrid automata, probabilistic automata. Students learn to work with the model checking tools Murphi and Uppaal.

• Software Specification

  Level and Type	Graduate, Undergraduate ; Laboratory, Lecture
  Developed By	Matthew Dwyer and John Hatcliff
  Offered At	Kansas State University ; Department of Computer Science
  Tools Used	Alloy, USE (UML), ESC/Java
  Materials Offered	Examples, Assignments, Handouts, Lecture Notes, PowerPoint slides, streaming video lectures, exams, weekly exercises and qu izzes
  Notes	The course emphasizes tool-based formal specification methods, and the distri bution for instructors includes a variety of pedagogical materials as described above. A separate distribution for students includes only the lecture slides a nd examples.

• Modelling Reactive Systems 4

  Level and Type	Undergraduate ; Lecture, Laboratory
  Developed By	Alice Miller
  Offered At	University of Glasgow
  Tools Used	Spin, SDL 2000, MSC 2000 and TTCN-3
  Text Used	The SPIN Model Checker: Primer and Reference Manual, GJ Holzmann, 2003, Addison- Wesley, ISBN: 0-321-228626
  Materials Offered	Lecture Notes; Assignments, Examples
  Notes	Course includes: Introduction to reactive systems: examples and problems. Basic modelling formalisms: Finite State Automata and State Transition Diagrams. The need for concurrency and communcation; synchronous and asynchronous communication. Message Sequence Charts. Introduction to State Based Formalisms. Promela (Process Meta Language) Major Protocol Example. Analysis Techniques: simulation, validation, temporal logic and model checking. SPIN workbench. Real time aspects of SDL 2000, MSC 2000 and TTCN-3

Software Modeling Courses

• Modeling Software Systems

  Level and Type	Graduate, Undergraduate ; Lecture
  Developed By	Egon Boerger
  Offered At	University of Pisa ; Department of Computer Science
  Tools Used	SMV, PVS, ASM executing engines (AsmGofer, XASM, AsmL)
  Materials Offered	Lecture Notes; Book
  Notes	For the book "Abstract State Machines. A Method for High-Level System Design and Analysis" (by E.Boerger and R. Staerk) and for accompanying lecture slides in ppt and pdf format see http://www.di.unipi.it/AsmBook.

• Formal Methods (ASM Method)

  Level and Type	Graduate, Undergraduate ; Lecture
  Developed By	Egon Boerger
  Offered At	University of Pisa ; Department of Computer Science
  Tools Used	SMV, PVS, ASM executing engines (AsmGofer, XASM, AsmL)
  Text Used	AsmBook
  Materials Offered	Lecture Notes; Book

• Formal Methods in Software Engineering

  Level and Type	Graduate, Undergraduate ; Lecture
  Developed By	Arthur Fleck
  Offered At	University of Iowa ; Department of Computer Science; Electrical and Computer Engineering
  Tools Used	Miranda, ZSL, Maude
  Text Used	Z an Intro to Formal Methods by Diller + readings in algebraic specification
  Materials Offered	Lecture Notes; Assignments, Handouts
  Notes	The course is also offered via streaming video on the Web.

• Modelling Reactive Systems 4

  Level and Type	Undergraduate ; Lecture, Laboratory
  Developed By	Alice Miller
  Offered At	University of Glasgow
  Tools Used	Spin, SDL 2000, MSC 2000 and TTCN-3
  Text Used	The SPIN Model Checker: Primer and Reference Manual, GJ Holzmann, 2003, Addison- Wesley, ISBN: 0-321-228626
  Materials Offered	Lecture Notes; Assignments, Examples
  Notes	Course includes: Introduction to reactive systems: examples and problems. Basic modelling formalisms: Finite State Automata and State Transition Diagrams. The need for concurrency and communcation; synchronous and asynchronous communication. Message Sequence Charts. Introduction to State Based Formalisms. Promela (Process Meta Language) Major Protocol Example. Analysis Techniques: simulation, validation, temporal logic and model checking. SPIN workbench. Real time aspects of SDL 2000, MSC 2000 and TTCN-3

Software Engineering Courses

• Software Engineering

  Level and Type	Graduate, Undergraduate ; Lecture
  Developed By	Perry Alexander
  Offered At	University of Cincinnati ; Department of Electrical/Computer Engineering, Department of Computer Science
  Tools Used	Z
  Materials Offered	Projects, Assignments, Handouts

• Advanced Software Engineering

  Level and Type	Graduate, Undergraduate ; Lecture
  Developed By	Perry Alexander
  Offered At	University of Cincinnati ; Department of Electrical/Computer Engineering, Department of Computer Science
  Tools Used	PVS, Larch
  Materials Offered	Projects, Assignments, Handouts

• Tutorial on Formal Methods

  Level and Type	Undergraduate ; Lecture
  Developed By	Dr. Ann E. Kelley Sobel
  Offered At	NIST ; government installation
  Materials Offered	course outline
  Notes	This was a 3-day formal methods tutorial presented at the National Institute for Standards and Technology. Dr. Black set the agenda, and Dr. Sobel developed the material and taught the course.

• Ingenieria de Software

  Level and Type	Undergraduate ; Lecture
  Developed By	Maximiliano Cristia
  Offered At	Facultad de Ciencias Exactas, Ingenieria y Agrimensura - Universidad Nacional de Rosario - Argentina ; Department of Computer Science
  Text Used	Ghezzi, C., Jazayeri, M. y Mandrioli, D., Fundamentals of Software Engineering, Prentice Hall, Upper Saddle River, 1991
  Materials Offered	Examples, Assignments, Handouts, Lecture Notes
  Notes	The course and the Web page are held in Spanish.

• Formal Methods (Z Notation)

  Level and Type	Undergraduate ; Laboratory, Lecture, Tutorial classes
  Developed By	Jonathan Bowen
  Offered At	The University of Reading ; Department of Computer Science
  Tools Used	ZTC, ZANS
  Text Used	See http://www.cs.reading.ac.uk/cs/people/jpb/teaching/z/books.html
  Materials Offered	Examples, Assignments, Lecture Notes

• Software Engineering II

  Level and Type	Undergraduate ; Lecture
  Developed By	Lawrence C Paulson
  Offered At	University of Cambridge ; Department of Computer Science
  Materials Offered	Lecture Notes
  Notes	An elementary course aimed at first year students, it introduces basic notions of program refinement, loop design with invariants, defensive programming, etc. There is a general lecture on formal methods, a lecture on Z, and a lecture on proving correctness of functional programs using structural induction.

• Java Programming and Concurrency

  Level and Type	Graduate, Undergraduate ; Lecture
  Developed By	Radha Jagadeesan, Konstantin Laufer
  Offered At	Loyola University Chicago ; Mathematical and Computer Sciences
  Tools Used	Triveni
  Text Used	Doug Lea, Concurrent Programming in Java, Addison-Wesley, 1997
  Materials Offered	Projects, Examples, Assignments, Handouts

• Internet Programming

  Level and Type	Undergraduate ; Lecture
  Developed By	Curtis Tuckey
  Offered At	Loyola University Chicago ; Mathematical and Computer Sciences
  Tools Used	MAWL, VoxML
  Text Used	CGI Programming on the World Wide Web, Shishir Gundavaram, O'Reilly
  Materials Offered	Projects, Examples, Assignments, Handouts, Lecture Notes

• CMU 15-671: Models of Software Systems

  Level and Type	Graduate, Masters in Software Engineering ; Lecture
  Developed By	David Garlan
  Offered At	Carnegie Mellon University ; Department of Computer Science, Master in Software Engineering Program
  Materials Offered	Assignments, Handouts, Lecture Notes

• Formal Specification of Software (CSC227)

  Level and Type	Undergraduate ; Laboratory, Lecture
  Developed By	Steve Riddle
  Offered At	University of Newcastle upon Tyne, UK ; Department of Computer Science
  Tools Used	IFAD VDMTools & Toolbox Lite
  Text Used	John Fitzgerald and Peter Gorm Larsen, "Modelling Systems: Practical Tools and Techniques for Software Development", Cambridge University Press 1998, ISBN 0521 62348 0
  Materials Offered	Examples, Assignments, Handouts, Lecture Notes
  Notes	The course provides an introduction to modelling data and functionality using VDM-SL, a model-oriented specification language. The stress is on practical modelling skills rather than language detail. The examples and coursework exercises are based on industrial applications and the tools support understanding of specifications by admitting execution of formal models. Some discrete math and some functional programming have been found to be useful prerequisites.

• Design and Analysis of Communication Software

  Level and Type	Graduate, Undergraduate ; Laboratory, Lecture
  Developed By	Patrice Godefroid in collaboration with David L. Dill
  Offered At	Stanford University ; Department of Electrical/Computer Engineering
  Tools Used	VeriSoft
  Materials Offered	Projects, Handouts

• Fundamentals of Software Engineering Mathematics

  Level and Type	Graduate ; Laboratory, Lecture
  Developed By	Janusz Laski
  Offered At	Oakland Univeristy ; Computer Science and Engineering
  Tools Used	VDM-SL Toolbox
  Text Used	Nimal Nissanke, "Introductory Logic and Sets for Computer Scientists"
  Materials Offered	Examples, Syllabus
  Notes	The course web page will be continuosly updated and new material will be included.

• Systematic Software Development

  Level and Type	Graduate, Undergraduate ; Laboratory, Lecture, Term Project
  Developed By	Janusz Laski
  Offered At	Oakland Univeristy ; Computer Science and Engineering
  Tools Used	VDM-SL Toolbox
  Text Used	J.Fitzerald, P.Larsen, "Modelling Systems: Practical Tools and Techniques in Software Development."
  Materials Offered	Projects, Syllabus
  Notes	The page will be updated by providing concrete project examples.

• Software Specification

  Level and Type	Graduate, Undergraduate ; Laboratory, Lecture
  Developed By	Matthew Dwyer and John Hatcliff
  Offered At	Kansas State University ; Department of Computer Science
  Tools Used	Alloy, USE (UML), ESC/Java
  Materials Offered	Examples, Assignments, Handouts, Lecture Notes, PowerPoint slides, streaming video lectures, exams, weekly exercises and qu izzes
  Notes	The course emphasizes tool-based formal specification methods, and the distri bution for instructors includes a variety of pedagogical materials as described above. A separate distribution for students includes only the lecture slides a nd examples.

• Formal Methods (ASM Method)

  Level and Type	Graduate, Undergraduate ; Lecture
  Developed By	Egon Boerger
  Offered At	University of Pisa ; Department of Computer Science
  Tools Used	SMV, PVS, ASM executing engines (AsmGofer, XASM, AsmL)
  Text Used	AsmBook
  Materials Offered	Lecture Notes; Book

• Formal Methods in Software Engineering

  Level and Type	Graduate, Undergraduate ; Lecture
  Developed By	Arthur Fleck
  Offered At	University of Iowa ; Department of Computer Science; Electrical and Computer Engineering
  Tools Used	Miranda, ZSL, Maude
  Text Used	Z an Intro to Formal Methods by Diller + readings in algebraic specification
  Materials Offered	Lecture Notes; Assignments, Handouts
  Notes	The course is also offered via streaming video on the Web.

Logic Courses

• Logic in Computer Science

  Level and Type	Graduate, Undergraduate ; Lecture
  Developed By	Moshe Y. Vardi
  Offered At	Rice University ; Department of Computer Science
  Materials Offered	Assignments, Handouts, Lecture Notes

• Tutorial on Formal Methods

  Level and Type	Undergraduate ; Lecture
  Developed By	Dr. Ann E. Kelley Sobel
  Offered At	NIST ; government installation
  Materials Offered	course outline
  Notes	This was a 3-day formal methods tutorial presented at the National Institute for Standards and Technology. Dr. Black set the agenda, and Dr. Sobel developed the material and taught the course.

• Formal Methods (Z Notation)

  Level and Type	Undergraduate ; Laboratory, Lecture, Tutorial classes
  Developed By	Jonathan Bowen
  Offered At	The University of Reading ; Department of Computer Science
  Tools Used	ZTC, ZANS
  Text Used	See http://www.cs.reading.ac.uk/cs/people/jpb/teaching/z/books.html
  Materials Offered	Examples, Assignments, Lecture Notes

• Logic and Proof

  Level and Type	Undergraduate ; Lecture
  Developed By	Lawrence C Paulson
  Offered At	University of Cambridge, England ; Department of Computer Science
  Materials Offered	Lecture Notes
  Notes	The lecture notes include examples and exercises.

• Computation and Deduction

  Level and Type	Graduate, Undergraduate ; Lecture
  Developed By	Frank Pfenning
  Offered At	Carnegie Mellon University ; Department of Computer Science
  Tools Used	Twelf logical framework
  Text Used	Course notes on "Computation and Deduction"
  Materials Offered	Projects, Examples, Assignments, Handouts, Lecture Notes
  Notes	The course provides an introduction to logic, type theory, reasoning about programs and programming languages using the formal meta-language Twelf as a tool.

• CMU 15-671: Models of Software Systems

  Level and Type	Graduate, Masters in Software Engineering ; Lecture
  Developed By	David Garlan
  Offered At	Carnegie Mellon University ; Department of Computer Science, Master in Software Engineering Program
  Materials Offered	Assignments, Handouts, Lecture Notes

• Formal Fault Verification

  Level and Type	Undergraduate, M.Tech , Pre - Ph.D. ; Seminar, Laboratory, Lecture, Recent Research Papers
  Developed By	Dr Aarti Gupta
  Offered At	Indian Institute of Technology Delhi India ; Department of Electrical/Computer Engineering, Department of Computer Science
  Tools Used	VIS, SMV
  Materials Offered	Projects, Examples, Assignments, Handouts, Lecture Notes

• Logical Foundations of Programming

  Level and Type	Undergraduate ; Lecture
  Developed By	Michael Huth
  Offered At	Kansas State University ; Computing and Information Sciences
  Tools Used	SMV
  Text Used	M. Huth and M. Ryan; Logic in Computer Science: modelling and reasoning about systems; Cambridge University Press, 2000.
  Materials Offered	Examples, Assignments, Handouts
  Notes	The textbook is supported by a website which features an online, multiple-choice tutor, instructional material, and more. It can be found at http://www.cis.ksu.edu/~huth/lics/

• Program Verification

  Level and Type	Undergraduate ; Lecture
  Developed By	Peter H. Roosen-Runge
  Offered At	York University ; Department of Computer Science
  Tools Used	suite of verification tools developed in Prolog (see text)
  Text Used	Software Verification Tools (unpublished)
  Materials Offered	Projects, Assignments, Handouts, Lecture Notes, text, _Software Verification Tools_, (PDF file)
  Notes	The focus of the course is the use of simple tools to support various aspects of software verification. The tools are: * wang -- uses method of sequents to check tautologies tautologies containing descriptive terms Applications: logic problems derived from English or mathematical statements. * simplify -- rewrite system used to implement arithmetic and abstract datatypes. Applications: verifying Forth and stack-based programs symbolic evaluation of functional expressions * prover -- combines simplify + wang + 'paramodulation' Applications: verifying identities on abstract datatypes; verifying implementation of one ADT by another. verification of refinement of Java interface specifications * induction -- uses prover to prove identities involving simple and tail-recursive functional expressions. * symbex -- uses wang and simplify to symbolically execute C/Java assignment and procedure statements, check assertions and generate post-conditions Applications: verifying straight-line assembler and loop-free C/Java code segments * wp -- derive Hoare-style pre-conditions from simple C/Java code: assignment, computations on array elements, conditionals, while-loops. Verify code segments annotated with invariant and variant specifications.

• Fundamentals of Software Engineering Mathematics

  Level and Type	Graduate ; Laboratory, Lecture
  Developed By	Janusz Laski
  Offered At	Oakland Univeristy ; Computer Science and Engineering
  Tools Used	VDM-SL Toolbox
  Text Used	Nimal Nissanke, "Introductory Logic and Sets for Computer Scientists"
  Materials Offered	Examples, Syllabus
  Notes	The course web page will be continuosly updated and new material will be included.

• Software Specification

  Level and Type	Graduate, Undergraduate ; Laboratory, Lecture
  Developed By	Matthew Dwyer and John Hatcliff
  Offered At	Kansas State University ; Department of Computer Science
  Tools Used	Alloy, USE (UML), ESC/Java
  Materials Offered	Examples, Assignments, Handouts, Lecture Notes, PowerPoint slides, streaming video lectures, exams, weekly exercises and qu izzes
  Notes	The course emphasizes tool-based formal specification methods, and the distri bution for instructors includes a variety of pedagogical materials as described above. A separate distribution for students includes only the lecture slides a nd examples.

Other Courses

• Formal Software Synthesis

  Level and Type	Graduate ; Seminar, Lecture
  Developed By	Perry Alexander
  Offered At	University of Cincinnati ; Department of Electrical/Computer Engineering, Department of Computer Science
  Materials Offered	Readings

• Advanced Formal Methods

  Level and Type	Lecture
  Developed By	Perry Alexander
  Offered At	University of Cincinnati ; Department of Electrical/Computer Engineering, Department of Computer Science
  Tools Used	Larch
  Materials Offered	Projects

• Specification Methods for Distributed Systems (with emphasis on LOTOS)

  Level and Type	Graduate ; Lecture
  Developed By	Luigi Logrippo
  Offered At	University of Ottawa (ON, Canada) ; Department of Computer Science
  Materials Offered	Lecture Notes
  Notes	Only a few classes are available on the Web.

• Logic Synthesis

  Level and Type	Lecture
  Developed By	Robert Brayton
  Offered At	University of California at Berkeley ; Department of Electrical/Computer Engineering
  Materials Offered	Projects, Assignments, Lecture Notes

• Introduction to Functional Programming

  Level and Type	Undergraduate ; Lecture
  Developed By	John Harrison
  Offered At	University of Cambridge ; Department of Computer Science
  Materials Offered	Lecture Notes, Slides from lectures

• Theory of Distributed Systems

  Level and Type	Undergraduate ; Seminar
  Developed By	Joachim Parrow
  Offered At	Royal Institute of Technology, Stockholm ; Teleinformatics
  Tools Used	Concurrency Workbench
  Text Used	Milner, Communication and Concurrency
  Materials Offered	Projects, Examples, Assignments, Handouts, Lecture Notes, Solutions to exercises, old exam problems

• Models for Digital Systems

  Level and Type	Lecture
  Developed By	Geert Janssen
  Offered At	Eindhoven University of Technology ; Department of Electrical/Computer Engineering
  Tools Used	BDD program, LTL satisfiability checker, fair-CTL model checker
  Materials Offered	Lecture Notes, Transparencies

• Formal Methods

  Level and Type	Lecture
  Developed By	David Gilbert
  Offered At	City University, London ; Department of Computer Science
  Tools Used	Z
  Text Used	Systems Construction and Analysis' by N. Fenton and G. Hill, McGraw Hill International, 1993
  Materials Offered	Assignments, Lecture Notes

• Programming Languages 1

  Level and Type	Graduate ; Lecture
  Developed By	Gary T. Leavens
  Offered At	Iowa State University ; Department of Computer Science
  Materials Offered	Assignments, Handouts, Lecture Notes, Readings, exams

• Principles of Programming Languages

  Level and Type	Undergraduate ; Lecture
  Developed By	Gary T. Leavens
  Offered At	Iowa State University ; Department of Computer Science
  Materials Offered	Assignments, Handouts, Lecture Notes, Readings, exams

• Semantic Models for Programming Languages

  Level and Type	Graduate ; Lecture
  Developed By	Gary T. Leavens
  Offered At	Iowa State University ; Department of Computer Science
  Materials Offered	Assignments, Handouts, Lecture Notes, readings

• Logic Programming

  Level and Type	Undergraduate ; Seminar, Lecture
  Developed By	Naomi Lindenstrauss
  Offered At	Hebrew University Jerusalem, Israel ; Department of Computer Science
  Tools Used	SICStus Prolog
  Text Used	Lloyd "Foundations of LP", Sterling Shapiro "The Art Of Prolog"
  Materials Offered	Examples

• Analisis de Sistemas

  Level and Type	Undergraduate ; Lecture
  Developed By	Maximiliano Cristia
  Offered At	Facultad de Ciencias Exactas, Ingenieria y Agrimensura ; Department of Mathematics
  Materials Offered	Examples, Assignments, Handouts, Lecture Notes
  Notes	The course and the Web page are held in Spanish

• Formal Software Specification Using RAISE

  Level and Type	Graduate ; Laboratory, Lecture
  Developed By	Chris George and other UNU/IIST staff
  Offered At	UNU/IIST ; Department of Computer Science
  Tools Used	RAISE tools
  Text Used	The RAISE Specification Language; The RAISE Development Method
  Materials Offered	Examples, Assignments, Handouts, Assignment solutions

---

This site is currently maintained by Kathi Fisler Department of Computer Science, Worcester Polytechnic Institute Last updated on Saturday, 24-Jun-2006 21:43:12 EDT Acknowledgements