22C:181 - Formal Methods in Software Engineering, Spring 2001

Resources

This page provides information on some of the resources available for students in 22C:181. The page is organized as follows:

1. Miscellaneous Resources: about the course, formal methods for Java, and formal methods in general.
2. Reserve List: A list of materials on reserve at the Mathematical Sciences Library

Miscellaneous Resources

The following are some links to various resources you may find useful about the course, formal methods for Java, and formal methods in general.

Course Resources

• The course documentation directory, including:
  • errata for Cohen's book.
  • A sample emacs customization file (.emacs).
• Meeting outlines directory, containing outline files for the "lectures".
• Lecture notes directory, containing strangely formatted notes for the "lectures". We recommend that students use the meeting outlines (above) instead.

Formal Methods for Java

• The Java modeling language (JML) home page.
• Extended Static Checking project at Compaq Systems Research Center.
• LOOP project from Bart Jacobs's group in Nijmegen.
• iContract, which supports specifications in javadoc comments.
• iDoclet, the iContract doclet.
• The Jass tool, which supports design by contract for Java.
• The Infospheres Java Coding Standard.
• Doclets written in Javadoc, some of which pertain to specification.
• DowWiz - The JavaDoc Documentation Tool.
• JUnit for Java test cases.
• Java PathFinder a model checker for Java programs.
• Bandera a model checker and model checking framework for Java programs.
• Mocha model checker home page.
• Daikon dynamic invariant detector.
• Hyper/J, a tool supporting "multi-dimensional separation of concerns" for Java.
• AspectJ, aspect-oriented programming for Java.
• Other Java tools.

Other Formal Methods Resources

• The World-Wide Web Virtual Library: Formal Methods.
• The Risks Digest: Forum On Risks To The Public In Computers And Related Systems and Illustrative Risks to the Public in the Use of Computer Systems and Related Technology.
• Alloy Constraint Analyzer, an object modeling notation and lightweight formal method.
• OCL page, of links concerning the Object Constraint Language.
• The Larch FAQ.
• IFAD's site for VDM-SL and related tools.
• Gary Leavens's favorite formal method links.

Return to top

Reserve List

To check out one of these (for a few hours or days), go to the Mathematical Sciences Library reserve desk. Take along the call number and title, or look up 22C:181 there.

Required Text

Required

Other Texts On Formal Methods

Return to top

Last modified Tuesday, May 8, 2001.