CS 292C: Applications of Formal Methods to Computer Architecture

FGPAs running in the cloud, custom TPUs in the datacenter, GPUs used for surgery -- we live in a world where architecture is not something computer scientists can afford to ignore.  All software abstractions—from the application logic, to language run-time, operating system, and virtual machine—in the end perform their function through a set of primitive operations on a physical device. This fact provides both significant challenges and opportunities to formal analysis. On one hand, hardware sub-systems implement the lowest level of computing abstraction and cannot be undercut by software implementation artifacts.  On the other hand, hardware is physical and failures (malicious or otherwise) may not constrained by the formal model that is used to develop or verify the hardware.  In this class we will review the state of formalism as applied to computer architecture looking at language and machine support, applications in parallelism, security, virtualization, and correctness.

Students will be expected to read the assigned papers (on the order of 3 to 4 papers per week), participate in class, and prepare presentations for a subset of the papers (at the rate of around once per week).  In addition there will be a term research project under which students are expected to apply and/or extend concepts from the course and present a working project.