Below are the links to the tools that we will use in the course. Each of these tools is available for Windows, Linux or Mac OS X platforms. If you want your own copy just download and install (its pretty easy).

• Alloy and its Constraint Analyzer are an object modeling language and analysis tool, respectively.
• USE is a UML-based tool that processes class diagrams and OCL specifications. Models conforming to the class diagrams can be animated and automatically checked against the given OCL specifications.
• Kiasan is a JML contract-based automatic verification and test case generation tool-set for Java.
  Download Kiasan here.