Its a good idea to check your grades on blackboard soon. Mail Peter (nvrnvrby@hotmail.com) with discrepancies.
I've posted a plain text and word copy of the study list for the final in the lecture notes directory (there's a link at the bottom left of the homepage). They are "CS 586 Objectives.doc" and "objectives.txt". The final will be three hours in the classroom on Wednesday from 230-530. I'll be out of town, but someone from the lab will come to proctor the exam.
Don't forget that you can fill out the online evaluatin of this class (listed as a 501R) for 1 extra homework credit. You must allow your name to be shown to get the credit. Not filling out the form and making your name available will not hurt your homework score.
you can run the nifty interface to SPIN by typing: ~jones/bin/xspin. Or if you have ~jones/bin in our path, you can just type xspin. There are some promela models in ~jones/Test/. Have fun!
It appears that my license for JPF does not permit use by third parties. Which, I believe, means I can't release it to the class. So we'll learn SPIN, and cover the "inline C" parts of the new spin. I'll demo JPF in class and we can discuss it, but I can't just dump it into the open labs for free use.
Don't forget that there's no class today! Class will meet Wednesday to watch the video. We'll meet Friday when I get back to discuss the discussion questions from the video worksheet.
As you know, I'll be at Super Computing in Phoenix part of next week. Here's the plan:
Monday: No class.
Wednesday: Watch first 1/2 of E. Dijkstra video and fill out worksheet. Be prepared to discuss how to do program verification, as described by Dijkjstra, using a model checker on Friday.
Friday: Discuss Dijkstra video and discuss last project.
The last project, project 6, will be due Tuesday 11/25 (which really means the 11/26 by 8am) which is the day before the break.
I will only have office hours from 10 to 1030 this morning. If you'd like to see me this afternoon, drop me an email at jones@cs.byu.edu
Mike.
I need to cancel my office hours from 3-4 this afternoon. I will still be reading email this afternoon and evening. If you have any questions, send me mail. Or, if you do MSN messenger (or something compatible) send me (jones@cs.byu.edu) your contact info and we can IM.
[schedule] the schedule has been updated so that... the BDD package is due next Wednesday (10/15), the Kripke to BDD translator is due the following wednesday (10/22) and the symbolic model checker is due the friday after that (10/31-Halloween!).
My office hours for Thursday morning need to be moved back to 130-230 pm rather than 10-11am. Other times are available by appointment.
We aren't going to spend another week on Kripke Structures. We will spend some time talking about the Kripke Structure parser, but that's it. We will start into temporal logics today or Wednesday. The reading will move up so that you should start reading chapter 3 now. I'll make the third homework due this Friday though (write a specification for a mutual exclusion protocol). The Kripke parser will remain where due next Friday (Sept 26).