CMSC 499A: Operating Systems as Abstract Machines
Fall 2026. Current UMD undergraduates may participate through CMSC499A: Research with Professorial Faculty. Interested students should email dvanhorn@cs.umd.edu before the start of the semester.
This research project will explore a new approach to teaching and building operating systems using the Lean programming language and theorem prover. Rather than beginning from low-level hardware mechanisms alone, we will investigate operating systems as implementations of higher-level abstract machines that provide programmers with processes, virtual memory, files, communication channels, and other protected abstractions.
The project will focus on designing and implementing a small executable operating-system model in Lean. We will begin by defining the semantics of an abstract user machine
that exposes programmer-visible concepts such as processes, message passing, scheduling, and shell interaction. We will then explore how these abstractions can be realized atop progressively lower-level machine models involving memory, privilege modes, traps, and virtual memory.
The emphasis of the study will be on:
- executable semantic models,
- systems programming in Lean,
- abstract machines and interpreters,
- operating-system structure and invariants,
- lightweight mechanized reasoning,
- and the relationship between high-level system abstractions and low-level implementations.
Students participating in the study may help design:
- the abstract process machine,
- a small process programming language,
- schedulers and memory managers,
- IPC and filesystem abstractions,
- a toy shell and runtime environment,
- and supporting infrastructure for a future course based on these ideas.
The project is intended to be highly exploratory and implementation-oriented. While Lean will be used throughout, the focus is not on large-scale formal proof engineering. Instead, we will emphasize executable models, semantic clarity, testing, and lightweight reasoning about system invariants.
Students with interests in programming languages, operating systems, formal methods, compilers, runtime systems, or semantics are especially encouraged to participate.