Overview:

This course is about the principles of software verification:  the theory and practice of systematically reasoning about the correctness of software.  In the class you will learn different techniques for writing down precise specifications of desired system behavior (“preconditions / postconditions / invariants”, “temporal logic”, “process algebra”) and for proving that specifications hold of software artifacts.  You will also learn about algorithmic approaches (“model checking”) for automatically establishing such correctness results.  Here is a tentative lecture schedule for the semester.

Instructor:

Rance Cleaveland (rance “at” cs dot umd dot edu)
4111 AV Williams Building
301-405-8572
Office Hours: MW 2:30 – 3:30, and by appointment

Time / Place:

3:30 – 4:45 MW, CSIC 2107

Text:

No required text; notes and suggested readings will be made available during the class.

Coursework:

Your workload, and its impact on your final grade, will be as follows.

1. Homework assignments (5 - 6)           20%
2. Midterm                                              20%
3. Final project                                        30%
4. Final exam                                           30%

Homework:

Homework assignments will be due the week after they are assigned, and will be returned graded as soon as possible.  Please note that late homeworks will only be accepted by prior arrangement.

Tests:

Both midterm and exam will be given in class.  The lecture schedule gives the dates.  .  Requests to take tests on alternative days will generally only be granted in the following circumstances:  (1) a student has a religious observance falling on the same day that conflicts with the announced test date, or (2) a student is participating in an official University-sponsored activity that conflicts with the announced test date.  Any such request must be made at least one week in advance so that alternative arrangements can be made.

In case of incapacitating illness on the day of a test, the student must contact his / her instructor as soon as possible, preferably by e-mail on the same day.  In this case, the student must produce, within one week of the original test date, a written note from a health-care professional attesting to the nature and severity of the illness.  The note must indicate the dates on which the student was incapacitated and a phone number for follow-up verification.  When this documentation is provided, alternative arrangements for the test will be made.  If no such documentation is produced within the given time frame, a score of 0 will be given on the test.

Final Project:

The course has a final project, which may take one of two forms. In the first, you will specify and verify a system of your choice either by hand or with the aid of one or more verification tools, and give a presentation in class summarizing your efforts. In the second, you will present a lecture summarizing the research findings contained in 2-3 research papers covering a particular topic in verification and validation.

Projects are group efforts, with teams consisting of 2-3 people.  Here is a list of suggested project topics.

Academic Integrity:

Unless explicitly allowed otherwise by the instructor, any assignment you turn in for grading must be your own work.  In particular, any work you submit as part of a project must have been written by you, and any solutions you prepare for a midterm or final exam must be exclusively of your own devising.  Any transgressions of these principles are violations of the campus Code of Academic Integrity and will be handled as such.  The webpage of the Student Honor Council contains a detailed explanation of what constitutes academic dishonesty, which includes not only cheating, fabrication, and plagiarism, but also helping other students commit acts of academic dishonesty by allowing them to obtain copies of your work.

Each case of suspected academic dishonesty will be referred to the University's Office of Judicial Programs. If the student is found to be responsible of academic dishonesty, the typical sanction results in a special grade "XF", indicating that the course was failed due to academic dishonesty. More serious instances can result in expulsion from the university. If you have any doubt as to whether a contemplated act of yours might constitute academic dishonesty, please consult one of the course instructors

Academic

Accommodations:

Any student eligible for and requesting reasonable academic accommodations due to a disability is requested to provide me a letter of accommodation from the Office of Disability Support Services (DSS) within the first two weeks of the semester.