Synopsis: In this course, we will study a collection of techniques for formal software development, spanning the whole development process: from high-level semantic modeling, to system architecture design, to coding and debugging. The study will be done not in the abstract, however, but through the use of actual tools supporting these techniques. In particular, we will study and use:

* the Alloy Constraint Analyzer, for semantic modeling and analysis,
* the USE tool, for system architecture design, and
* the ESC/Java static checker, for code analysis and debugging.