Synopsis: CISC422 is an introduction to the formal specification, design, and automatic analysis of software artifacts. The course presents a variety of specification notations (propositional and predicate logic, Z, Alloy, UML/OCL, temporal logic), and discusses corresponding analysis techniques (theorem proving, constraint checking, animation, model checking) using existing commercial and research tools (Jape, Z/Eves, Alloy, USE, SMV). The course compares the various approaches and attempts to balance theory (e.g., discussing theorems) and practise (e.g., discussing tools).