search
Table of Contents
The CS 686 course teaches model checking as applied software verification. Software verification using model checking is a very important topic for concurrency and input; it provides a tool that essentially proves a program correct under any input or any schedule in the presence of concurrency. In the simplest form, model checking constructs an exhaustive proof through state space enumeration. That is to say that a model checker checks every reachable state of a program under every input and schedule. Such a naive approach quickly succumbs to state explosion in all but trivial programs.
This course focuses on recent advances in model checking to reduce the number of states that need to be enumerated in order to prove a program correct. These advances include symbolic execution, bounded model checking, counter example guided abstraction and refinement, dynamic partial order reduction, parallel and distributed model checking, and proofs of termination/non-termination. The topics are selected with an emphasis on techniques that provide working tools. The hope is to gain practical experience with software verification that is informed by insights from studying the underlying technology.
The course is centered on seminal papers describing different technologies for software model checking. With each seminal paper is an accompanying tool that grew out of the original work. The homework is to use the tool in a way that exploits the strength of the approach and its inherent weakness in an effort to better understand the underlying technology.
Content
- Software model checking
- Symbolic execution
- Counter-example guided abstraction and refinement
- Bounded model checking
- Dynamic partial order reduction
- Parallel and distributed model checking
- Proof of termination or non-termination
Objectives
At the end of the course, an active engaged student is able to
- name the broad classes of techniques for software verification and explain the intuition behind their operation;
- discuss considerations in choosing a software verification technique as it relates to data non-determinism, scheduling non-determinism, and the property of interest;
- apply software verification techniques to simple programs using existing tools; and
- identify areas of potential research to extend existing techniques in software verification.
Prerequisites
None.
Text Book
None
Grade Composition
Policies
Retakes
Students are allowed only one retake of any class. If a student withdraws from or fails a class a second time, the student will not be allowed to register for any CS course for one semester (or one term, if in spring or summer). This policy does not apply to classes dropped before the add/drop deadline.
After one semester (or term), a student must petition to be allowed to take CS courses again. The petition must provide evidence of a substantive change that makes success in future CS classes much more likely. For example, a student may have demonstrated success in technology, math, or science-based courses. The petition will be reviewed by the undergraduate advisor.
Petitions for non-academic (e.g., medical or military) exceptions to the one semester/term waiting period may be granted according to university policies. Information about filing a petition can be found here: http://cs.byu.edu/retake-policy
Grade Appeals Policy
If you disagree with any grade, submit your grievance via email to the instructor, documenting the merits of your case, and the instructor should respond via email. For a grade dispute to be considered, the written grievance must be submitted in writing within two weeks of when the respective quiz, project, or exam is returned.
Late Policy
There is a 10% on the final graded point value for each day late for the first 7 days. Items are not accepted after 7 days. Monday is the same as Sunday for counting late days. As such, a submission on Monday is graded as if submitted on Sunday. Each student is given 3 free late days to use anytime in the semester for homework. A late day postpones the homework a single day. Late days can be applied anytime in the semester and there is not extra credit for not using the days. All homework and projects are due by midnight on the posted date.
Test Policy
Please make sure to arrange your schedule to accommodate the tests. If you need to miss a scheduled test, then you will need to document legal or medical emergency. A test is available in the testing center as indicated in the schedule. You are responsible for knowing when the testing center opens and closes. The outcome of a missed exam with no legal or medical emergency to justify the situation is determined by individual circumstances after careful discussion with the instructor.
Academic Honesty
The Honor Code includes a statement of standards regarding academic honesty. Academic honesty includes completing your own homework and exams unless there are express instructions to work in a group. The outcome of betraying academic honesty is determined by individual circumstances after careful discussion with the instructor.
Preventing & Responding to Sexual Misconduct
In accordance with Title IX of the Education Amendments of 1972, Brigham Young University prohibits unlawful sex discrimination against any participant in its education programs or activities. The university also prohibits sexual harassment—including sexual violence—committed by or against students, university employees, and visitors to campus. As outlined in university policy, sexual harassment, dating violence, domestic violence, sexual assault, and stalking are considered forms of “Sexual Misconduct” prohibited by the university.
University policy requires all university employees in a teaching, managerial, or supervisory role to report all incidents of Sexual Misconduct that come to their attention in any way, including but not limited to face-to-face conversations, a written class assignment or paper, class discussion, email, text, or social media post. Incidents of Sexual Misconduct should be reported to the Title IX Coordinator at t9coordinator@byu.edu or (801) 422-8692. Reports may also be submitted through EthicsPoint at https://titleix.byu.edu/report or 1-888-238-1062 (24-hours a day).
BYU offers confidential resources for those affected by Sexual Misconduct, including the university’s Victim Advocate, as well as a number of non-confidential resources and services that may be helpful. Additional information about Title IX, the university’s Sexual Misconduct Policy, reporting requirements, and resources can be found at http://titleix.byu.edu or by contacting the university’s Title IX Coordinator.
Students with Disabilities
Brigham Young University is committed to providing a working and learning atmosphere that reasonably accommodates qualified persons with disabilities. If you have any disability that may impair your completing this course successfully, please contact the University Accessibility Center (422-2767). Reasonable academic accommodations are reviewed for all students who have qualified documented disabilities. Services are coordinated with the student and instructor by the UAC. If you need assistance or if you feel you have been unlawfully discriminated against on the basis of disability, you may seek resolution through established grievance policy and procedures. You may contact the Equal Employment Office at 422-5895, D-282 ASB.
