CS 536, Fall 2018: Science of Programming http://cs.iit.edu/~cs536

Class Meetings

Disability Policy

Students with disabilities requiring academic accommodations should contact the Center for Disability Resources (disabilities@iit.edu, 312.567.5744). Please do this well in advance of needing an accommodation.

Staff Information (Last updated Aug 28)

Role Person Office Hours
Instructor http://cs.iit.edu/~sasaki
TA Tue 3-4 pm, Thu 1-2 pm, SB 004, x7-5149
TA Tue 4-5 pm, Thu 4-5 pm, SB 019a

This Page, Not Blackboard

Blackboard will be used to submit work and to list grades, but links to lecture notes, assignments, etc. will be on this page.

Course Goal

To learn the basics of software verification: How does verification differ from testing? How do we understand the semantics of programs, and how does that affect the way we understand program correctness? What rules of reasoning can we use to verify the correctness of everyday statements like assignment, decision, and iteration statements? What happens if we look at parallel programs? Can we approach the problem of parallel programs in steps? What if program execution isn't deterministic?

Academic Honesty

Students are responsible for maintaining the highest level of academic integrity as discussed in the IIT Code of Academic Honesty. The normal penalty for a violation of this policy for a non-final exam is a score of zero, with no Test Score Replacement (see below); for the Final Exam, the penalty is a final grade of E. In either case, Academic Honesty and the student's advisor and/or department (or other relevant administrators) will be notified.

Stay in Touch!:

Take advantage of the instructor and TA office hours, email, Piazza etc., whenever you have problems or questions. If you find yourself getting that lost feeling, don't wait — see the instructor.

Class Schedule (Last updated Dec 2)

The schedule below includes information on lectures, tests, and assignments. Dates are added or changed when an entry is added or changed, so check the schedule often.

Lectures: You're expected to attend or stream lectures and to keep up with them. Attendance will be taken intermittently (for internet students, we look at access dates on Blackboard). It can be used at the end of the semester as a tie-breaker for the final grade. The Handout / Reading column indicates lecture readings (possibly as links to files). Lectures may include in-class activities; these are generally not graded or reviewed, but can be. Solutions to activities (if posted) are appended to the notes.

Tests: The final exam date is set by the registrar. The dates of other tests and the materials covered by the tests are pretty firm [8/23], but it's possible they might be tweaked, so keep an eye out. The final exam will be comprehensive, with an emphasis (to be announced) on later material. The material covered on other exams is listed below. There's more information on test policies below.

Tests for Internet Sections: If you're in the Internet section, then if you want to, you can take tests on main campus with the live class. (No need for advance permission; just show up.) If you're outside the Chicago area or you want to take your test off-campus, contact the Office of Digital Learning well in advance to arrange for a proctor. (India Internet students should coordinate with IIT India for test times and locations.) If you need to take a test at a nonstandard time, contact the instructor well in advance for permission.

Assignments: Links to assignment handouts and information on due dates are included below. The number and timing of assignments may change as time goes on. If posted, solutions are appended to the assignment handout. More information on assignments is below.

Date Type Event Handout / Reading Note
Mon 8/20 Info Fall Classes Begin
Mon 8/20 Lec 1 Review Propositional Logic Lec_01.pdfAug 18; 24; Sep 20
Wed 8/22 Lec 2 Review Predicate Logic Lec_02.pdfAug 18; 24
Sun 8/26 HW 1 Post: Lec 1-3: Review logic; exprs and states HW_1.pdfAug 26; Lec 3 not yet covered
Mon 8/27 Lec 3 Expressions, States Lec_03.pdfAug 18
Wed 8/29 Lec 4 Satisfaction, State Updates Lec_04.pdfAug 28; 29; Sep 20
Mon 9/3 Holiday Labor Day - No Classes
Wed 9/5 Lec 5 Pgm Lang Syn + Op Sem Lec_05.pdfSep 4; 5
Wed 9/5 HW 1 Due: Lec 1-3: Review logic; exprs and states HW_1_soln.pdfSep 10
Wed 9/5 HW 2 Post: Lec 4-5: Sat, state updates, op semantics HW_2.pdfSep 7; 7
Mon 9/10 Lec 6 Denotational Sem, Runtime Errs Lec_06.pdfSep 9; 10
Wed 9/12 Lec 7 Sequential Nondeterminism Lec_07.pdfSep 16
Mon 9/17 Lec 8 Hoare Triples, pt.1 Lec_08.pdfSep 16, 18
Wed 9/19 Lec 9 Hoare Triples, pt.2 Lec_09.pdfSep 18
Wed 9/19 HW 2 Due: Lec 4-5: Sat, state updates, op semantics HW_2_soln.pdfSep 20
Mon 9/24 Exam 1 Material in Lec ≤ 5, HW ≤ 2 X1_stats.txtOct 15
Wed 9/26 HW 3 Post: Lec 6-9: Errs, Seq. non-det., Hoare triples HW_3.pdfSep 26
Wed 9/26 Lec 10 Strength; wp pt.1 Lec_10.pdfSep 22, 28
Mon 10/1 Lec 11 wp pt.2, Domain Predicates Lec_11.pdfOct 1
Wed 10/3 HW 3 Due: Lec 6-9: Errs, Seq. non-det., Hoare triples HW_3_soln.pdfOct 12, 17
Wed 10/3 Lec 12 Syntactic Substitution (started on Oct 1) Lec_12.pdfOct 1, 3
Mon 10/8 Holiday Fall Break Day - No Classes
Wed 10/10 Lec 13 Forward Assignment; sp Lec_13.pdfOct 3; 21
Thu 10/11 HW 4 Post: Lec 10-12: strength, wp, substitution HW_4.pdfOct 11, 16
Mon 10/15 Lec 14 Correctness Proof Rules pt.1 Lec_14-15.pdfOct 17
Wed 10/17 Lec 15 Correctness Proof Rules pt.2 Lec_14-15.pdfOct 17
Wed 10/17 HW 4 Due: Lec 10-12: strength, wp, substitution HW_4_soln.pdfLate HW in by noon Oct 18 // Oct 18, 21
Wed 10/17 HW 5 Post: Lec 13-15: sp, proof rules HW_5.pdfOct 21, 29, 31
Mon 10/22 Exam 2 Material > X1, Lec ≤13, HW ≤ 4 X2_stats.pdfOct 31
Wed 10/24 Lec 16 Corr. Proofs & Outlines pt.1 Lec_16-17.pdfOct 23; Nov 2
Mon 10/29 Lec 17 Corr. Proofs & Outlines pt.2 Lec_16-17.pdfOct 23; Nov 2
Wed 10/31 Lec 18 Loop Convergence Lec_18.pdfNov 1, 2
Wed 10/31 HW 5 Due: Lec 13-15: sp, proof rules HW_5_soln.pdfNov 17
Wed 10/31 HW 6 Post: Lec 16-17: proof outlines HW_6.pdfNov 1, 12
Mon 11/5 Lec 19 Finding Invariants; Examples Lec_19.pdfNov 4
Wed 11/7 Lec 20 (Find inv); Array Assignments Lec_20.pdfNov 4
Mon 11/12 Lec 21 Parallel and Disj Par. Pgms Lec_21.pdfNov 12, 14
Wed 11/14 Lec 22 Auxiliary Variables Lec_22-23.pdfNov 24
Wed 11/14 HW 6 Due: Lec 16-17: proof outlines HW_6_soln.pdfNov 24
Wed 11/14 HW 7 Post: Lec 18-22: Conv., Inv.,, Array asgt, Parall HW_7.pdf
Mon 11/19 Lec 23 Auxiliary Variables Lec_22-23.pdfNov 24
Wed 11/21 Holiday Thanksgiving Break (no class)
Mon 11/26 Lec 24 Shared Vars and Interference Lec_24.pdfNov 25
Wed 11/28 Lec 25 Synchronization: await Lec_25.pdfNov 25
Wed 11/28 HW 7 Due: Lec 18-22: Conv., Inv.,, Array asgt, Parall HW_7_soln.pdfNov 29, Dec 2
Sun 12/2 Info Last Day to Request an Incomplete
Wed 12/5 Exam (Final) 8 - 10 am, Hermann Hall Ballroom (South end)
10-20% on X1 material, 30-40% on X2, and
50-60% after X2 (lectures 14-25).
Wed 12/12 Info Final Grades Due at Noon

Textbooks, Assignments, and Activities

No Required Textbook

One possible reference is 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 material in the course is adapted 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 buy this book: It's expensive and its very difficult to follow (it's aimed for a more theoretical audience than ours).


If you have an emergency or are ill, it may be possible to excuse you from an assignment or to get you an extension, but contact the instructor (or have a friend or family member contact the instructor) as soon as you can. Please don't wait. Overly delayed requests may be denied. You can't get a retroactive extension on work you've already turned in or once the semester ends.

Assignments and Activities are Important!

It's important to do the assignments and lecture activities because they will help you prepare for the tests. If solutions to written questions are posted, they are appended to the assignment or lecture handout.

Late or Malformed Work

Work may be handed in up to two days late with a 5% penalty for one day late and a 10% penalty for two days late. (Saturday and Sunday count as days.) After this, work can be discussed but it earns a score of 0. You can't turn in a bunch of things at the end of the semester and get them graded.

It is your responsibility to make sure that you submit what you intend to submit and that what you submit is readable. If you submit a bad or unreadable assignment, etc., you may earn a penalty anywhere from a point off to no credit at all.

Work With Others; How to Submit

You're encouraged to work [8/26: in groups of ≤ 4] on assignments. Submit your answers just one time: Pick someone from your group and be sure to include the names and A-id numbers of all the group members at the top of the submission. Don't submit as a group; each person should submit separately. Submit using the Assignment folder on Blackboard; a pdf is best. (A scan of a handwritten solution is okay.) You can submit up to five times. If you submit more than once, we'll grade the last submission, so submit the entire assignment every time. You can also turn in work in class. If it's open, you can turn in work at the CS office (in that case, please get it time-stamped).

Test Policies

Tests: Closed Notes

Tests are closed-book, closed-notes. No books, phones, calculators, or other aids or devices are allowed (except for accommodations specified by the disability office).

Makeup Tests

If you're going to be out of town the day of a test, arrange for a change in test times well in advance. If, during a test, you feel too ill to finish it, stop and come up and talk to the instructor so we can work on rescheduling it — you can't retake a test once you turn one in. It might be possible to get a makeup test if you miss a test due to illness or other emergency, but contact the instructor as soon as possible. Overly delayed requests may be denied; requests made after the end of the semester will be denied.

Test Score Replacement

If you earn a bad score for Exam 1 and / or 2, the Final Exam will give you a chance to recover. For n = 1, 2, if your Final Exam score is greater than your Exam n score it will get used it as your Exam n score when calculating end-of-semester scores. (The replacement gets done when calculating end-of-semester scores; the exam score shown on Blackboard doesn't change.) The Final Exam will include a review of the material from Exams 1 and 2 that (on average) the class did badly on.

Test and Assignment Regrades

For test regrades, see the instructor. For assignment regrades, see the TA who graded it before seeing the instructor. Requests must be made before the final exam and within a week of receiving a grade. (For the final exam, the deadline is two weeks after the final grade is announced.) Requests must be specific, not for a whole problem or assignment or test. Requests must include a justification [8/23] based either on the quality of your work or on a mechanical error [8/23] like adding up your points incorrectly. "Needing" more points is absolutely not a justification.

Final Grade Policies

Final Grade Calculation

End-of-Semester Score: 10% Average of Assignments // 25% each Exams 1 and 2 // 40% Final Exam.(All scores are scaled to 100.)

Final Grade Cutoffs: A: 90-100; B: 80-89; C: 60-79; E: < 60. You can also earn an E by having an average Assignment score < 30% or Final Exam score < 40. Grade cutoffs are only rarely changed (and never downward).

The Ph.D. Section (CS 536-02): To receive credit for the Languages part of the written qualifiers, earn a final grade of 'A' and be in the top 25% of the class rankings.

Final Grade Measures Quality of Work

The final grade describes the quality of your work, nothing else. It can happen that you work hard but still earn a bad final grade. It can happen that earning a bad final grade puts you in a painful position or even causes a disaster. Personally, I feel bad for you, but professionally, I can't use any such troubles to affect your final grade.

For fairness's sake, students should all have the same opportunities do to the coursework, so you can't retake exams and you can't get extra credit work to improve your final grade. So, if on am exam day you're feeling ill, don't take the exam, see what grade you've earned, and then explain that you were feeling ill. Similarly, if you want an incomplete, talk to the instructor before the final exam and don't take the final exam. (If you've taken the final exam, it's harder for me to justify to the administration that your work was incomplete.)

Borderline Final Grades

I look for every reason I can find to push you up to the next higher grade, such as a very high Final Exam score or an increasing slope on test scores. If you're two points short on the Final Exam, I'll give you the benefit of the doubt. If you're five points short, expect the lower grade. (That's two exam points, not two EOS points.)

Final Grade Curving

In general, I like the class average Final Grade to be a low B.If a curve is needed, it's done by adding a constant > 0 to everyone's final score. Individual exams etc. don't get curved. I don't know what curve there will be until the end of the semester.

Posted Sun Dec 2, 2018; Copyright © 2018; James Sasaki, Illinois Institute of Technology. xhtml css