Models of Software Systems

Scientific foundations for software engineering depend on the use of precise, abstract models and logics for characterizing and reasoning about properties of software systems. A number of basic models and logics over time have proven to be particularly important and pervasive in the development of software systems. This course is concerned with that body of…

Logic for Systems

Mathematical logic provides the foundation for a rich set of tools for reasoning about systems and discovering whether their behavior meets our expectations. These tools allow us to model (e.g.) the state of buffers and caches, prove whether our protocols obey desirable properties, explore the consequences of memory-management strategies, and much more. As a Computer…

How to make Chord correct (with a surprising invariant)

The Chord distributed hash table (DHT) is well-known and often used to implement peer-to-peer systems. Chord peers find other peers, and access their data, through a ring-shaped pointer structure in a large identifier space. Despite claims of proven correctness, i.e., eventual reachability, “Using lightweight modeling to understand Chord” (Pamela Zave; ACM SIGCOMM Computer Communication Review,…

One day Allloy workshop

Most software flaws come from one of two places. When the code doesn’t match our expectations, it could be that the code is wrong. Most software correctness techniques – types, tests, etc – are used to check the code. But it could instead be that the code is correct and our expectations are wrong: there’s…