| Objectives |
Students taking this course can expect to acquire an
understnading of the following:
How to do proofs in Hoare Logic, and what
role a loop invaraint plays
How to use finite automata to model computer systems
How to express properties of concurrent systems in a
temporal logic
How to use a model checker to verify / falsify a
temporal safety property of a concurrent system
The connection between types and program
properties
|
| Contacting the Course Staff |
- For email and the newsgroup: please allow about 24 or so hours
for a response, except on weekends (see below).
- The staff do not work on the weekends. If you send something late
Friday or over the weekend then you should not expect a reply before
Monday.
- Never ever EVER call any staff at
home.
|
|
Instructions for Submitting Assignments
|
Each student is given an svn directory that needs to
be checked out at the beginning of the semester to as follows:
| mkdir <working_directory> |
|
svn co
https://subversion.ews.illinois.edu/svn/sp14-cs477/<your_netid>
<working_directory>
|
|
After the initial checkout, <working_directory>
will contain a subdirectory assignments. Once an
assignment (mp or hw) has been announced, if you do an
you will add a directory named after the assignment
(e.g. mp1) in the mps
directory. That directory will contain instructions for
the assignment, plus a stub for each file you must turn
in.
To do an assignment, you will need to follow the
instructions given in the directory for that
assignment. There will be two kinds of assignments, mps
and hws. Mps will be exercises carried out on tools
supporting a specific type of formal methods. Hws will be
written assignments proving theorems and doing hand
calculations. Since the mps involve using various tools,
by default you will need to do them on the ews linux
machines. Most of the tools should also be avialable form
the web to download to you own machine should you choose
to work on your own machine.
To submit an assignment, once you have completed the
necessry files as decribed in the assignment
instructions, in the assignment directory or either of the
parent directory or the gradparent directory
|
svn commit -m "<your comment here>"
|
|
You may restrict svn commit to a specific
collection of files and directories by adding a list to
the end of the command.
You may do multiple commits; the version that is in
the repositry at 11:59pm on the due date is that one that
will be collected and graded.
|
| Extensions |
- Each MP/HW will normally have an automatic 48-hour
extension with a penalty on that MP/HW of 20% the total value of
the assignment. If we cannot give such an extension for a
particular MP/HW, for example due to scheduling constraints, we
will announce that when the MP/HW is handed out.
During the automatic extension, staff is not obliged to
answer questions for that MP/HW. You are on your own.
Extensions without a point penalty for the first 48 hours and any
extension beyond the 48 hours will only be granted under very
unusual circumstances such as a medical or family emergency.
A signed note from a responsible party will be required.
If you do need such an extension for some legitimate reason,
do your best to let us know as soon as possible, preferably before
the normal MP/HW deadline.
|
| Regrade Policy |
|
Our goal as the course staff is to grade your work carefully and
accurately. Unfortunately, occasionally staff may overlook something,
misunderstand an otherwise correct answer, or record a score incorrectly.
This is where the regrade procedure steps in.
In order to have your regrade considered you must provide the following:
- your netid;
- what assignment or exam question was graded incorrectly; and
- why you think your answer deserves more points than what the
grader gave.
You must also submit your regrade request for a particular assignment
within one week of receiving grades for that assignment. It
must be submitted directly to the course instructor, not to the
TAs. Late regrade requests will not be accepted or read.
Good reasons to ask for a regrade:
- You used a notation that was unfamiliar to the grader but is
standard (e.g., in a textbook for one of your other courses).
- The grader recorded a score incorrectly.
- The problem was ambiguous (or just plain wrong), causing you to
interpret it differently than the grader.
- The grader marked the problem wrong incorrectly.
Bad reasons to ask for a regrade:
- Part of your answer "matched" the answer given in the solution.
A partially correct answer is still wrong.
"The difference between an
almost right word and a right word is the difference between a
lightning bug and lightning." -- Mark Twain
- You wrote down two or more answers, only one of which was correct.
Never put more than one answer for a question unless we tell you that
such a thing is legitimate.
- You expended a lot of effort answering the problem. We are
measuring mastery, not effort.
- You wrote something down.
|
| Collaboration |
|
You are allowed to collaborate on the machine problems (MPs) and
the written homework (HWs) of this course, in order to figure
out how to solve the problem, resolve things you don't
understand, and help each other track down errors or bugs.
Nevertheless, you must each write and test your code
separately and submit your own MP separately.
Similarly, you must write up and submit your own HW separately
from others.
If your collaboration extended beyond understanding for what the
problem was asking, then you should note on your assignment with
whom you collaborated. If you used sources other than the
course slides and assignment description for more than general
information in solving your problem, you should cite your
sources. As always, you are subject to the rules for
plagiarism. Whether you pass this course or not will depend
heavily on whether you pass the exams -- and those are
non-collaborative.
We allow you to collaborate for several reasons:
- all research done indicates that students learn more when they are
allowed to work together;
- our own ability to respond to student questions is increased
because your peers are able to give help.
However, you have to collaborate intelligently in order to get the most
out of it. If you ask a friend to describe the solution completely to
you and then write it down (in substantially different form), you will
get the credit but you'll fail the exam because you never learned the
methods/techniques/concepts.
If you copy a friend's solution directly or substantially, that
will be considered cheating, unless you give a clear cite of your
source. If you work as a group, each
writing part and sharing it with the others, that is also
considered cheating, unless your cite all members from whom you
copied. The penalties for being discovered
cheating are described in the next section, below. If you offer
your solution for others to copy, you should protect yourself
from being accused of cheating by reporting this as well. Then,
if some of those to whom you have lent your work fail to cite
you, you will be protected from cheating accusations (unless
they also claim they lent the same problem to you).
If you copy your solutions from friends or other sources, you
must cite your source.
Think of MPs and written assignments as being part of the
practice for the exam. Many of the problems will be used as a
basis for the exam problems themselves. In fact, when it comes
time to study, we will likely advise you to redo your MPs and
written assignments.
|
| Policy on Cheating |
|
We will be looking for cheating on both homeworks and exams. The
penalty for being caught cheating a first time -- either sharing your
solution on an exam, or copying someone else's solution (without
citation, if it is a homework) -- is that you will receive a negative score
for the unit cheated on equal to the value of the unit. A homework
(MP or written assignment) is one unit. A numbered problem on test,
including all its parts, is a unit. The penalty if you are caught
cheating a second time is a grade of F for the class. Moreover, if
you cheat a second time, both cheating episodes will be reported to
the department. You should take all reasonable precautions to prevent
others from cheating and report any suspected cheating.
|
| Grading |
|
Our goal is to have grades back to you as soon as possible. In
practice, this will probably take about a week for each
assignment or exam. Whenever your homework is graded, it will
be placed in your svn repository, the grade reported on compass,
and message will be placed on the class website.
Do not ask when grades are available. They will
be in your repository and on compass when they are available.
Exams this semester will be take-home and will be given out
submitted and returned via the svn repository in the same manner
as the assignments.
| Grading Breakdown |
|---|
| Work |
Weight |
Notes |
| Machine Problems and Written Assignments (combined) | 30% |
| Midterm | 30% |
| Final Exam | 40% |
| Project | NA |
Only for 4-unit graduate students |
|
| Textbooks |
|
There is no required textbook for this course. However, the following textbooks are recommended reading: (see also the resources page)
|
|
|