Overview:

This course covers principles of algorithmic checking of whether or not a system satisfies a mathematic specification given for its behavior.  Specific topics to be covered will include most if not all of the following list:  propositional and predicate logic; SAT and SMT solving; temporal logic; Kripke structures; finite state machines; Buechi automata; lattices and fixpoints; timed automata; hybrid automata; model-checking tools.  Here is a tentative lecture schedule for the semester.

Prerequisites:

Permission of CS Department

Instructor:

Rance Cleaveland
4111 AV Williams Building
rance “at” cs umd edu

301-405-8572

Office hours:  M 2-3, Tu 2-3

Time / Place:

3:30-4:45 TuTh / CSI 2118               

On-Line Discussion Forum:

This class will be using a Piazza web-site for on-line discussions, questions, posting of homework assignments, etc.  The link is https://piazza.com/umd/spring2017/cmsc838m/home.  Make sure you have access to this site; any who do not should contact the instructor.

Text:

There is no required textbook.

Coursework

and Grading:

Course work is as follows, together with how it will be weighted for final grades.

1. Homework                                          20%
2. Midterm exam                                                20%
3. Project                                                30%
4. Final project                                       30%

Grades will be assigned based on the following anticipated ranges, which may be expanded based on what happens during the semester.  The lower and upper parts of each range will be reserved for +/- grades.

The CS Department’s grades server will be used to record grading information.

Homework:

Homework assignments will be made weekly, and will be due on the date indicated on the assignment.  Late submissions will only be accepted by prior arrangement only!

Exams:

The midterm will be administered in class.  The lecture schedule gives the date.  The final exam may be given in class, on the date given in the lecture schedule, or administered instead as a take-home exam during finals week.  The decision about this will be announced later in the semester.

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.

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.

Project:

The course has a final project, which may take one of two forms. In the first, you will use or modify tools to specify and verify a system of your choice. 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 up to three people.  Here is a list of project ideas; feel free to develop your own.

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 one of the course instructors.

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.

Academic

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 Office of Disability Support Services (DSS) 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.