EECS 755

Software Requirements Modeling and Analysis


EECS 755 Blog


Welcome to the EECS 755 blog for Spring 2020. You will find late-breaking information about the class and associated projects and exams here. The blog is available via RSS feed if you use an RSS aggregator.

As you’re getting started it would be a good idea to installed Coq on your system of choice. If you are not an emacs and linux user, it is strongly suggested that you use CoqIDE to get started. Is the name implies it provides a drag-and-drop installation as well as a graphic interface for Coq. Should you become a power user, you will eventually want to move to emacs and ProofGeneral.

Homework Instructions

Before starting anything else, get Coq installed and running on a machine you have access to. There are many ways to do this (see the homepage for a few). The easiest way to do this is install the Coq IDE, but the best ways are using emacs or VSCode as a frontend. Coq must installed before proceeding.

I will be assigning problems from Adam Chlipala’s Formal Reasoning About Programs (FRAP) text referenced on our class homepage. The problem sets and a bunch of support files including the text are available via a github repo at:

When you do your clone of this repo, use the recursive option to install the FRAP book and libraries:

git clone --recursive

In the resulting repo you will find a directory frap that contains the Frap.v library, the FRAP text, and acompanying FRAP Coq files. Descend into this directory and run make to build the book and libraries. The build takes awhile, so be patient.

You will also find a file in the base directory that contains instructions for using the problem sets.g If you don’t install and build the frap submodule above, none of the problem sets will work properly.

I will go through most of this in class, but please try to get Coq and the problem sets installed on your own. It’s helpful to have tried all this once before you see it live.