Specification and Verification Tools Seminar (Fall 2008) Information

This page gives access to information about the Specification and Verification Tools Seminar as taught (in Fall 2008) by Gary T. Leavens for the School of EECS at the University of Central Florida. The seminar's home page is http://www.eecs.ucf.edu/~leavens/spec-tools-seminar/. This page, which describes the seminar, is organized as follows.


Meetings will be held every Wednesday at 2:30pm to 3:20pm in 356 Harris Center.


You can of course attend without registering for an independent study.

However, if you wish to take the seminar for credit, you can sign up for an independent study by contacting Gary T. Leavens (leavens@eecs.ucf.edu).

Students who sign up for 3 credits of independent study will select and present at least two (2) systems to the seminar, and lead at least four (4) meetings of the seminar, which will include leading the seminar in some exercises. Exercises will be due the week before the start of the system's discussion, so that other participants can try them out.

Students taking the seminar for credit will also write up a report on each tool they present, describing the goals of the tool, how to install and use the tool, introductory examples, a case study, related work, and an evaluation. The report should be scholarly, and must properly credit and cite all materials used.

Independent study for this seminar will be graded on a S/F basis.


This seminar is for those doing research on tools to help specify and verify software systems. The idea is to get background on the state of the art in software support for reasoning about software.


The only prerequisites are interest in formal methods and software tools.


Initial plans are to study some or all of the following: Alloy, Event-B, Spark/Ada, Spec#, JStar, Bandera, and others suggested by participants.

Last modified Thursday, June 25, 2009.