Synopsis: This course emphasizes tool-based formal specification methods and focuses on Alloy (5 weeks of lecture material), OCL/USE (5 weeks of lecture material), and ESC/Java (2 weeks of lecture material). A downloadable archive is available for instructors that includes a variety of pedagogical materials such as PowerPoint lecture slides, links to streaming video recordings of lectures, sources for lecture examples, weekly quizzes and solutions, homeworks and solutions, and exams and solutions. A separate distribution for students includes only the lecture slides and examples.