CS 536 Syllabus (S'23, IIT)

Course Goals

Learn the basics of software verification:

• How does verification differ from testing?
• How do we understand the semantics of programs?
• How does semantics affect the way we understand program correctness?
• What rules of reasoning can we use to discuss program correctness?
• How is correctness of parallel programs different?
• What if program execution isn't deterministic?

Textbook

References (optional)

There's no required textbook; we'll have handouts instead, available on the website. Unfortunately, there's no great book to use for the course; they're mostly more advanced than we'd want. That said, here are a couple of very optional references:

• The Science of Programming, by David Gries, Springer-Verlag, © 1981. Unfortunately the book uses weird notation and has a number of typographical errors and doesn't include everything we'll be covering.
• Most of the course material comes from Verification of Sequential and Concurrent Programs (3rd edition), by Krzysztof R. Apt, Frank S. de Boer, and Ernst-Rüdiger Olderog, © 2009, Springer-Verlag. But don't get this book: It's expensive and written for a very theoretical audience.

Logic References (Optional)

If you want to review propositional and predicate logic,

1. One reference is online at myIIT Library > Databases > Books 24x7. Search for Fundamentals of Discrete Math for Computer Science: A Problem-Solving Primer by Tom Jenkyns and Ben Stephenson, Springer © 2013.  Study Sections 3.2 (Boolean Expressions and Truth Tables) and 3.3 (Predicates and Quantifiers).

2. There is a CodeGuage site with an Elementary Logic course. A quick spin through that might be helpful. Unfortunately, it seems they only discuss predicates with outermost quantifiers. (E.g., ∃x.∃y.p, but not predicates like (∃x.p) → (∃y.q).)

3. There's a handout at Cornell that is a more detailed introduction to predicate calculus. Two notes: We write (e.g.) (∀x.P) ∧ ∃y.Q where they write (∀x)(P ∧ (∃y)Q). We write logical equivalence as "⇔"; they use LE ↔ .

Exams

Material Covered

Roughly: Exam 1 will cover the first third of the semester; Exam 2 will cover the middle third of the semester. The Final Exam will be comprehensive but will emphasize the final third of the course. It will also repeat topics from the earlier exams that on average received low grades. One sheet of notes is allowed. (See Exam Notes on the homepage.)

Exam Score Replacement Policy

If your Exam 1 or Exam 2 score is low, it can be improved by doing better on the Final Exam. For Exam n (n = 1 or 2), the exam score used at the end of the semester is the larger of the earned Exam n score and the Final Exam. (The exam score shown in Blackboard is not changed.) Note it's possible for the Final Exam to be used for all three exams. You can't substitute Exam 1 ↔ Exam 2 scores and you can't substitute Exam n → the Final Exam. (By the way, having this policy is why the final exam re-covers less-well-understood material)

Homework Assignments

There will be ≤ 11 homework assignments. All assignment problem sets will be posted on the course website and submitted via Blackboard. Assignment submissions must be typed up (diagrams may be created in your diagramming software of choice) and in PDF form. Scans of handwritten work will not be accepted. Unless specified otherwise, the assignments are equally weighted.

Group Work

You're to work in groups of three on assignments. You can choose whom to work with or be assigned randomly to groups. It's not required that everyone in the group do exactly the same kind of work, but everyone should contribute roughly equally. (Note: Discussing problems counts as work, not just writing up answers.)  To encourage everyone in the group to participate, all three people are required to submit a short writeup of what each of the three of you did. (So three descriptions of three people's work, but hopefully not like Rashomon.)  For a short period at the beginning of the assignment period, you can start a new group or join an existing group by changing your group number. The size = 3 limit still applies. Note you can only change your group number, not someone else's.

What to Hand In

Your answers: They must be a typed-up pdf, not a scan of hand-written answers or a Word file, etc. Submit one set of answers for the whole group. (You decide who will submit.) Include answers for all the questions. (Don't submit some problems and then some other problems.) If you submit multiple times, we'll grade only the last one. Include the name and A-id numbers of all the group members at the top of your submission. Each assignment will have its own Blackboard Assignments folder for submissions.

For the group work report, each of you submit your own file. Include everyone's name and A-ID (but highlight which one you are) and include which assignment the report is for. The group reports for all the assignments go into one single "Group Reports" folder.

Late Assignments

Unless otherwise specified, work is due at 11:59 pm Chicago time on the specified day. (Chicago is on Central Standard Time (CST = UTC -6) through the end of the semester.). Late assignments, unless cleared in advance with the instructor, are subject to a 5% reduction in points per each day late. After 1 week (7 days) past the due date, an assignment can be reviewed for correctness but won't receive any points.

For homework due just before an exam, late submissions may be disallowed so that correct answers can be discussed before the exam.

Missing Classes, Homework, or Exams

When to Contact the Instructor

In general, missing a lecture or two or leaving a lecture early is not an issue, and you don't need to discuss this with the instructor (unless you wish, of course). If you know you will miss a future exam or homework, however, contact the instructor ahead of time. Similarly, if you're ill or have an emergency the day we have an exam or an assignment due, contact the instructor or have someone else contact the instructor as soon as practical.

Extensions and Makeups

In most cases, homework extensions can be given for illness, travel, or emergencies. (But not for "I'm really busy".)  Make your request as soon as practical: Excessively late requests risk being denied. You can't resubmit a homework assignment after it's been graded, and barring really severe circumstances, makeups for missed homeworks are not given. You can resubmit homework before it's due, however: see What to Hand In, above.)

If you miss an Exam it may be possible to schedule a makeup, but again, contact the instructor promptly. If you miss Exam 1 or 2 and don't make it up, the exam score replacement policy applies. On the other hand, you can't retake an exam. In particular, don't take the Final Exam if you're sick that day; ask for a makeup instead.

Malformed or Wrong Submissions

It's your responsibility to turn in the right work and that it be readable, so if you submit the wrong file or a garbled pdf, you may earn a penalty or even no credit at all.

Grading Questions

Once grades for a homework or Exam 1 or 2 are announced, you have two weeks to dispute the grading. For the Final Exam, the limit is one week. If a teaching assistant graded the work, discuss the situation with the assistant before contacting the instructor. You can only have specific problems regraded, and you must have some concrete issue with the grading.

Examples: "For problem 3, my solution is a correct alternative" is ok; "For problem 3, my answer would be correct if you made this small tweak to it, so I think it's worth more than 0 points" is probably still ok; and "Regrade HW 8 -- I'm sure I earned more points" gets rejected. Note the new grade can be lower than the old one, if an earlier unnoticed error is found.

Final Grades

Grading Philosophy

I don't think of myself as "giving" grades; students "earn" grades based on the overall quality of their work. So at the end of the semester, I look at the pile of work you did and look to discover its overall quality, as measured by your end-of-semester score.

End-of-Semester Score

Your end-of-semester score is is a weighted sum of your homework average and your exam scores. (If necessary, scores are rescaled to percentages.).

• 10% : Homework Assignments
• 25% : 1.25 hr Exam 1 or Final Exam score (whichever is higher).
• 25% : 1.25 hr Exam 2 or Final Exam score (whichever is higher).
• 40% : 2 hr Final Exam score

Letter Grades

The end-of-semester score cutoffs for the letter grades are A: 90%-100%,  B: 80-89%,  C: 60-79%,  E: 0-59%. In addition, you earn an E if your Final Exam score is 35 or less.

Final Grade Curve

If the class average end-of-semester score maps to less than a low B, I may curve it by adding a nonnegative constant to everyone's end-of-semester score. I avoid manipulating the grade boundaries if I can.  Individual exams and assignments are not curved.

If You're Close to a Grade Border

If you're within a couple of Final Exam points (FX, not EOS points) short of the next grade, I just push you up.  If you're five points short of the next grade, you'll almost certainly get the lower grade.  Otherwise, I start looking for reasons to raise your grade by trying to think of all the reasons you might give to argue for a higher grade. If I can find one, I push your grade up.  For example, if your Final Exam score was significantly above average, that really helps you.  If your three exam scores increased over time, that helps some.  The class average homework score is always pretty high, so your homework average would have to be close to perfect to help you.

Can't You Just Raise My Grade? (Sigh, Of Course Not.)

It's unfortunate, but you can work very hard for a course and still earn a low grade, which can lead to extremely unpleasant consequences for you.  Again unfortunately, those consequences absolutely can't be a factor in the final grade.

Sometimes people ask "Can't you just raise my grade?," then I say no, and they say, well, it never hurts to ask.  But that's really not the case.  Raising your grade would cheat the other students, so asking that question actually asks me to cheat the other students.  That's why some instructors take it as a personal insult to be asked.  For my own part, I take them as requests coming from students so focused on their troubles that they don't realize what they're really asking.

The Ph.D. Section and Qualifying Exam Waivers

Students in CS 536-02 (the Ph.D. section) can earn a waiver for the Languages portion of the written Ph.D. qualifying exam by earning an A in the course and being in the top 25% of students in the class. Ph.D. students who want a waiver but need to take the course via internet should sign up for section 02 but watch the lecture videos.

Course Incompletes

If you want an incomplete for the course, talk to the instructor as soon as you can. Don't take the Final Exam: You can't get an incomplete if you do. In any case, be aware of the university's deadline for requesting incompletes.

Academic Honesty

For homework, all group members should contribute roughly the same amount to the result.  This doesn't mean that each must solve exactly one-third of the problems or write exactly one-third of the submission; it means that the discussion and writing efforts involved should be comparable.

With this course as structured, for homework, dishonesty comes down basically to not copying information from the web (or other sources) without clearly saying that it was indeed copied and from where.  For exams, dishonesty usually comes from copying someone else's answers, with or without their permission.  You're allowed one sheet of notes, so using more than that is also dishonest.  For more discussion on what constitutes academic dishonesty consult the university's Code of Academic Honesty.

Handling Academic Dishonesty: Any confirmed cases of academic dishonesty will be officially reported.  Any homework involved will (at the very least) receive a reduction in grade deemed appropriate by the instructor.  Cheating on exams earns a grade of E for the course.  (Unfortunately, 11 students did that in Fall 2022.)

Title IX Policy

The Office of Title IX Compliance oversees Illinois Institute of Technology’s response to Title IX Sexual Harassment within the university. For information, see https://www.iit.edu/title-ix.

Disability Accommodations

Reasonable accommodations will be made for students with documented disabilities. To obtain a letter of accommodation, contact the Center for Disability Resources at https://www.iit.edu/cdr.