EECS 755

Software Requirements Modeling and Analysis


EECS 755 Blog

Zoom Password

It appears the default setting for zoom chats was changed from no password to requiring a password. This was the right thing to do. Zoom bombing is becoming more and more popular. Unfortunately, I did not see the announcement of the new policy if there was a formal announcement. I assume there was and take full responsbility for people not being able to join class today.

For subseqent classes, the zoom link with password is:

Zoom Link

IndProp File

I just pushed a fresh version of the IndProp.v file I was going through in class today that does not use constructor or econstructor in the proofs I went over today. Use apply for now and will learn the constructor commands once you’re comfortable with apply and inductive relations.

Exam Visibility

I believe you should now be able to see your exam results. I changed visibility options on Blackboard and hope I changed the right ones!

Midterm Exam Topcs

I just posted a list of exam topics and some general guidance for the midterm on the class page. It is my intention to hold the exam during our class period, but it will be done online. As suggested in class, I will have a zoom session open during the exam period so you can ask questions.

If you have concerns, please let me know. I want you all to do well!


I just posted the last 4 lectures on Blackboard. Thanks to whomever made that suggestion - it worked great!

April 7 Class

I just pushed an update to the class slide deck and added a new Coq file to the class repo. The Coq file is called IndProp.v and contains examples for class discussion. The slide set contains new slides that contain a subset of information from the Coq file. Pull the repo and you’ll be ready to go.

Bring your Pset15 questions to class. Stop being shy about asking questions!

GitHib Link Fixed

I fixed the link to our class GitHub repo on the course hompage. It should be Sorry if the bad link caused you difficulties!

Everything is graded

Everything that has been submitted to Blackboard has now been graded. All-in-all, the class did very well - pretty much what I expected.

March 31 Class

Information for our March 31 clss. We will use the same ID as last week, 513-078-938 and will begin at 2:30. I will turn on chat and the hand-raising thing which seemed to work well last week.

We will be working through three things: (i) pset15; (ii) section 4.3 from the FRAP book; and (iii) Chapter 5 on Transition Systems from the FRAP book. I will update the slide deck in the class repo with new material. Please have the FRAP book, Interpreters.v and TransitionSystems.v handy as we will use those as well.

pset15 is your next homework assignment and we’ll talk about that in class Tuesday. It is an extension of what we’ve done with interpreters over the last several lectures. As always I will leave time in class for anwswering project questions before the due date. We will decide on a due date tomorrow.

Pset15 Added

I just added pset15 to the class git repo. We will talk about it in class. If you want to get started, starting with pset14 would be a good idea. As you prove the compiler correct, you may use my approach that uses the distribution lemma or Chlipala’s approach that does not.

GitHub Repo

Just updated the 755 GitHub repo to include pset14 with solutions. Also did a bit of reorganization. I’m working on getting the lecture video pushed over, but not quite there yet.

Really only one rule for the repo - don’t share it. Chlipala’s work is licensed and solutions to his problem sets should not be made public.

Please send me your GitHub ID if you want access and I’ll add you.

March 26 Class

Information for our March 26 class. We will use the same meeting ID as Tuesday, 513-078-938, and will begin at 2:30. I will turn on chat and the hand-raising indicator. Not sure what I’ll do with chat yet as it might be distracting for me to watch as I present, but I think it’s great that you are using it.

We will be working through a slide set outline that I will post before class; section 4.3 of the FRAP book; and interpreters.v starting with the definition of the cmd abstract syntax. I don’t expect you to read all this before class, but wanted to give you a heads up so you can have the files downloaded and ready to go.

I intend to hold office hours right after class to answer questions. We’ll see how that works, but it should go fine.

Class Tuesday

We will start EECS 755 again March 24 online using Zoom at or normal class time, 2:30. I will be presenting roughly the same as before, just using Zoom instead of a projector. We will be continuing our discussion of compiler verification and then move to transition systems.

Before break we spoke of an exam. We will need to discuss that further. I am committed to making sure you are evaluated fairly, but will need to be a bit more imaginative than required in the past. I’m looking at options and will share with you when I’ve got proposals to choose from.

I believe Zoom will work fine, but I have not used it in this way before. Please be patient as I work out the kinks. I’ve never presented from a computer in class before and that seems to work fine, so hopefully this will go well. Here are the contact details for the class meeting:

EECS 755
24 Mar 2020 at 2:30 PM - 3:45 PM

I will do my utmost to make certain you have a good experience for the remainder of the semester. The show must go on!

Pset3 due date clarification

Since my last post I’ve learned that we are not allowed to require things to be due during this second break week. So to clarify, Pset3 will be due next Tuesday, March 24. I will update the submission site to indicate this. Feel free to turn the assignment in early, but it is not formally due until the 24th.

I will have more information on how class will happen later this week. I’m still figuring out exactly how I want to use zoom. I will do a full dry run this Friday before we officially start holding classes, so I should be prepared to lecture on the 24th. It’s still going to be weird, but we will persevere.

Class Going Forward

As I’m sure you are aware KU has announced there will be no classes next week and classes after next week will be online.

In the near term, Pset3 is due on Tuesday and we were talking about an exam shortly after that. I would like you to go ahead and submit your assignment on Tuesday if possible. Should you have any issues with that, please contact me and we will work something out. Pset4 will not be your next assignment, although it certainly would not hurt to work through it. If you decide to work on it, be warned it is significantly harder than Pset3. Significantly harder in the sense that I have talked with no one who has completed it.

I will post your next assignment, Pset15, sometime this weekend or next week. It is a continuation of compiler verification we’ve been doing in class. I will ask you to extend the source language and the target language for the compiler to add conditionals and state. We will discuss the assignment in class before I assign a formal due date. It’s a really cool project that I’m excited for you to work on.

I have not figured out the exam yet. When I get lecture delivery figured out I will explore options for that. The simplest thing would be a take home exam, but I would like to consider other options.

Class going forward will be done online using Zoom. KU provides free access to Zoom and I have used it extensively. It is very nice and easy to use. However, I have never done a Zoom conference with 25 people before, so there may be some hiccups getting started. I’m doing everything I can to make sure that won’t happen, but bear with me during the first lecture or two as I work out the kinks. I will post the Zoom meeting link when I have it for you.

Office hours will be done using Zoom. I can also do advising with Zoom for any of my advisees who need to enroll this coming week.

It would be great if you could make sure you have Zoom installed and ready to go before the first day of resumed classes. KUIT can help with this as can ITTC.

Hang with me as we get restarted. I will do everything I can to make sure you have the chance to learn everything you would have given no pandemic.

Pset14 udpate

I just updated the pset14 tarball to fix a minor problem with the Makefile. No changes to any of the specification files or the infrastructure. The Makefile updates removed 2 files that are no longer present in the project.

No Class Next Week

As announced in class Thursday, there will be no lectures on Feb 25 or 27. I am traveling to a DARPA PI meeting and will not be back until Thursday afternoon. Remember that Pset2 is due in the 25th at 11:59. From my interactions with the class it seems you’re doing well. Pset3 will be next if you want to get started ahead of time.

Induction Examples

Induction examples from today’s class have been updated to include proofs. Please look at the last two examples before class on Thursday so we can push ahead quickly.

Stack Specifications

I’ve added the Stacks.v file with specifications of several stacks from class to the class repo and to the website under Class Notes. We will be adding to it a bit over the next few weeks, but this will give you an opportunity to play with the specs and try out techniques I showed you in class.

There are two stack specifications at the end of the file we have not gone over in class. One uses option and the other uses functions to prevent trying to pop or find the top of empty. You are welcome to play with these. Don’t fret - I will go over them in class.

Load Path

If Coq is having problems finding the Frap library (or any other library) you can define where it should look for files. The directive is:

Add LoadPath "path/to/file".

where path/to/file is a Linux pathname. Don’t forget the quotes.

Homework File Download

I have fixed the link to specifications I’ve been doing ineractively in class. Filenames now use underscores and the URLs are building correctly. Class notes files are named XXX_class.v.

Homework Instructions

I will be assigning problems from Adam Chlipala’s Formal Reasoning About Programs text referenced on our class homepage. The problem sets are available via a github repo at:

In the resulting repo you will find a that contains instructions for using the problem sets. Make sure you follow the instructions for installing the frap submodule under Building Problem Sets or nothing will work right. You may also need to define the shell variable COQBIN using the provided script.

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.


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.