This course covers formal methods used in the development of software. It studies languages for object-oriented modeling, such as the Unified Modeling Language (UML) along with its Object Constraint Language (OCL) and Action Semantics extensions; the specification of abstract data types, such as Z; and concurrency, such as process algebras and temporal logic.