The course teaches modern compiler techniques applied to general-purpose or domain-specific languages.
This course explores means of documenting the semantics of programming languages. Through a series of exercises using the Coq theorem prover, it studies the semantics of simple programming languages and gradually build up to a study of a Java-like object-orient programming language.
The course covers techniques for developing high assurance systems -- systems that are safety critical, security critical, or mission critical in nature.
This course studies a collection of techniques that lie at the foundation of an approach to software development that can enable the construction of large highly reliable software.
This course studies various model-checking techniques with the goal of applying those techniques to real concurrent software systems.