Logic for Hackers

Spring 2014

Computer Science Department

Brown University

Who

Instructors
Tim Nelson
Shriram Krishnamurthi

TAs
Spencer Gordon (HTA)
Cody Mello
Kenny Micklas
Vikram Saraph

When

MWF 10-11
CIT 368

Assignment Schedule

Office Hours

Files from Class

List of Final Projects

Textbook

Software Abstractions by Daniel Jackson

Electronic copy from Brown Library

Software

We will use Alloy.

  1. Please download and install Alloy 4.2 onto your machine ASAP. (Yes, unfortunately, this means you'll need to install Java.)
  2. In the configuration, please change the setting for Forbid overflows from off (which is the default) to on. (On OS X, go to the Options menu and select the last entry. Nothing will appear to happen, but when you look at the menu again, the setting will be on.)

Collaboration

You may not discuss your work with anyone other than course staff, except a partner on a group assignment. You are responsible for keeping your files secure, etc.

Background

Logic plays a central role in describing systems. In addition, logic offers the foundation for a rich set of tools for reasoning about systems, namely, determining whether they have been described correctly relative to our expectations.

Unfortunately, this fascinating set of activities can come across to some as rather drab and pedantic. In turn, logic often fails to take hold of computer science imaginations because it seems to be a collection of statements about the state of Socrates and rain, not about the state of buffers and caches and the other difficulties that everyday practicing computer scientists wrestle with.

This course attempts to address this problem by re-focusing logic on computer systems. We will use logic to describe systems and then analyze our descriptions of them. We will use modern tools that ease the description and automate the analysis. In the process we will try to re-imagine the way we think about not only describing but even designing complex modern computer systems.