Topics in Specification and Verification for Java-like Languages Seminar (Com S 610 GL, Spring 2007) Information

This page gives access to information about the Seminar Topics in Specification and Verification for Java-like Languages (Com S 610 GL) as taught (in Spring 2007) by Gary T. Leavens for the Department of Computer Science at Iowa State University. The seminar's home page is http://www.cs.iastate.edu/~leavens/JML-spec-verif-seminar/. This page, which describes the seminar, is organized as follows.

Information about previous offerings of seminars related to JML is also available.

Meetings

Meetings will be held every Monday at 1:10pm to 2:00pm in 217 Atanasoff Hall.

Credit

If you plan to attend, and haven't already done so, please send email to Gary Leavens (leavens@cs.iastate.edu).

You can sign up for 1 credit if you like by registering for course 610 GL. Students who are registered for credit will be expected to contribute by presenting a paper and leading a discussion on it, and also by writing and presenting some specifications. (Grading is S/F only, of course.)

You can also attend without registering if you wish.

Background

This seminar is intended for those doing research on such topics, especially such topics related to the Java Modeling Language (JML). (We will also look at some papers related to Spec#, a similar language designed by Microsoft Research for C#.) JML is an international, cooperative research project, which is becoming widely-known in the formal methods community. It combines ideas from the Eiffel and Larch traditions and seems to be a practical approach to the specification of detailed designs. See http://www.jmlspecs.org for descriptions of the groups involved in the project, and the tools that they have produced that work with JML.

Prerequisites

Students are expected to have a working knowledge of formal methods and JML. Those without this background should read the tutorial paper Design by Contract with JML available from http://www.jmlspecs.org. If you have had Com S 512 and/or knowledge of formal methods this should be sufficient. See Gary Leavens if you have questions.

Plans

In addition to unscheduled presentations by members of the local formal methods community on current work, the plan is to read various papers related to JML and its semantics, to try to improve the state of JML's documentation, and to try to improve specifications of the JDK. JML is an open source project, and students are welcome to, but not required to, contribute their specifications to the JML project.

Last modified Wednesday, January 17, 2007.