This course allows students to complete a graduate-level course in Cybersecurity Policy and Risk Management program via independent study if they were unable to take the course when it was offered. This course can substitute for a required course.

Formal languages and formal techniques for syntax analysis and parsing; organization of the compiler and its data structures; code generation. LL and LR parsing; automatic generation of scanners and parsers from high-level descriptions. Implementation of features from imperative and object-oriented languages. Students are required to design and implement a compiler for a simple language. Prereq: Machine Organization.

Introduction to fundamental concepts of computer networks and exploration of widely-used networking technologies. Topics include principles of congestion and error control; network routing; local, wireless and access networks; application protocol design; and network programming. In-depth discussion of the Internet suite of protocols.

Course focuses on the formal specification and verification of reactive systems, most notably concurrent and distributed systems. Topics relevant to these systems, such as non-determinism, safety and liveness properties, asynchronous communication or compositional reasoning, are discussed. We rely on a notation (T LA+, the Temporal Logic of Actions) and a support tool (TLC, the TLA+ Model Checker). Prereq: Students are expected to be knowledgeable in logic and to be able to write symbolic proofs in predicate calculus. A basic understanding of the notions of assertion, precondition, and post-condition is also assumed.