CMSC 630 / 498G Spring 2018

Foundations of Software Verification

Syllabus

 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: TuTh 2:00 – 3:00, and by appointment

Time / Place:

3:30 – 4:45 TuTh, CSIC 3120

Text:

There is no required text; notes and suggested readings will be made available throughout the semester.

Coursework:

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

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:

The midterm exam will be given in class; the final exam will probably be a take-home exam.  The lecture schedule gives the dates.  Requests to take tests on different 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.

Final Project:

The course has a final project.  Projects are group efforts, with teams consisting of 3-4 people. More information about the project will be released later in the semester.

The remainder of the syllabus contains information about course policies.  These are derived from campus-wide policies that may be found at http://ugst.umd.edu/courserelatedpolicies.html.

Academic Integrity:

Unless stated otherwise by the instructor, any assignment you turn in for grading must be your own work.  In particular, any code 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 a course instructor.

Excused Absences:

It is the student's responsibility to inform the instructor during the first two weeks of the semester of any intended absences from exams or class for religious observances.  Absences related to official University events must be brought to the instructor’s attention at least one week in advance of the absence.  In case of absences due to illness or other extenuating circumstances, the instructor should be notified as soon as possible, and appropriate documentation explaining the circumstances surrounding the absence should be provided.  See the university-policy page for more details on this point.

Accommodations:

Pursuant to university policy, any student eligible for and requesting reasonable academic accommodations due to a disability is requested to provide his or her instructor with a letter of accommodation from the University Accessibility and Disability Service (ADS) within the first two weeks of the semester.  Note that arrangements for individual exams must be made with the instructor at least one week in advance.