Fall 2025 Courses

This is a graduate course in operating systems. The course will consist of a reading/lecture/discussion component and a project component. The class will cover approximately 40 research papers. Some of these papers will introduce students to the basic principles on which modern operating systems and distributed systems are based. Others will cover more recent work to explore the state of the art and observe the evolution of these systems over time.

Resource use—the amount of time, memory, and energy a program requires for its execution—is one of the central subjects of computer science. Nevertheless, resource use traditionally does not play a central role in programming-language concepts, such as operational semantics, type systems, and program logics. This course revisits these concepts to model and analyze resource use of programs in a compositional and mathematically-precise way. The emphasis is on practical, type-based techniques that automatically inform programmers about the resource use of their code. We first study such techniques for functional programs and then develop generalizations to imperative, probabilistic, and concurrent programs.

Theoretical and practical aspects of building optimizing compilers that e¿ectively exploit modern architectures. The course will begin with the fundamentals of compiler optimization, and will build upon these fundamentals to address issues in state-of-the-art commercial and research machines.

The course covers a broad set of topics in algorithms design and analysis. The goal is to cover tools and algorithms that give students the ability to (a) recognize which tool or method to apply to problems, (b) to become reasonably proficient at using these tools, and (c) to be able to reason about the correctness and performance of the resulting algorithms. The course webpage for this semester will list the tentative list of topics to be covered; these will include basic graph algorithms, randomized algorithms, hashing and streaming, flows and linear programming, convex optimization, and linear algebraic algorithms. Please refer to https://www.cs.cmu.edu/~csd-grad/courseschedules22.html for the most recent schedule updates.

The course studies the theory of type systems, with a focus on applications of type systems to practical programming languages. The emphasis is on the mathematical foundations underlying type systems and operational semantics. The course includes a broad survey of the components that make up existing type systems, and also teaches the methodology behind the design of new type systems.

Automated reasoning has become a powerful technology with applications ranging from verification of hardware and software to solving long-standing open problems in mathematics. This course covers several state-of-the-art automated reasoning techniques and provides hands-on experience with research questions in this area.

This is a course exploring research issues in mobile computing and its close relative, pervasive computing (aka "Internet of Things (IoT)"). Many traditional areas of computer science and computer engineering are impacted by the constraints and demands of mobile and pervasive computing. The course will offer significant hands-on experience: students will work in small groups under the guidance of a mentor on a project. Each student will present a research paper from the literature in a conference-style 30-minute talk. In teams of two, students will present a short (30 minutes) overview of the commercial landscape for one of the topics covered in class. There will a brief quiz at the start of each class, based on the readings for that class. Prerequisites Knowledge of operating systems, distributed systems, and computer architecture. If in doubt, check with one of the instructors before registering.

The course covers advanced algorithms for learning, analysis, data management and visualization of large datasets. Topics include indexing for text and DNA databases, searching medical and multimedia databases by content, fundamental signal processing methods, compression, fractals in databases, data mining, privacy and security issues, rule discovery, data visualization, graph mining, stream mining.

This course is aimed as an introduction to modern cryptography. This course will be a mix of applied and theoretical cryptography.

In designing computer systems one is usually constrained by certain performance requirements and limitations. For example, one might need to guarantee a response time SLA or certain throughput requirement, while at the same time staying within a power budget or cost budget. On the other hand, one often has many choices: One fast disk, or two slow ones? More memory, or a faster processor? A fair scheduler or one that minimizes mean response time? For multi-server systems, one can choose from a wide array of load balancing policies, a wide array of migration policies, capacity provisioning schemes, power management policies ... The possibilities are endless. The best choices are often counter-intuitive. Ideally, one would like to have answers to these questions before investing the time and money to build a system. This class will introduce students to analytic stochastic modeling with the aim of answering the above questions.