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…

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…

What if you could find complex bugs in systems without ever having looked at any of the code, without running the code, without cloning the code, or even knowing what language the code is written in or where its git repo lives? What if you could validate the correctness of an architectural proposal before writing…

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,…

Alloy is a language and a toolkit for exploring the kinds of structures that arise in many software designs. This article aims to give readers a flavor of Alloy in action, and some examples of its applications to date, thus giving a sense of how it can be used in software design work.

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…

This site explores the Alloy specification language and its application with the Alloy Analyzer.