• PROMELA and the SPIN model checker
• Modeling systems using Kripke Structures
• Creating Kripke structures from programming languages
• Temporal logic for property specification including LTL and CTL
• Model checking using automata and language intersection
• Implementing fairness in model checking
• Model checking by Tableau
• Reduced ordered binary decision diagrams (ROBDDs)
• Symbolic model checking using ROBDDs
• The SPIN Model Checker
• Java Pathfinder

By studying the course contents and engaging in the homework, students are able to:

• Develop models with PROMELA and use the SPIN model checker to verify properties of those models
• Write specifications and properties in temporal logic
• Describe and implement the algorithms and data structures used in symbolic model checking.
• Explain the steps and implement the algorithms used for on-the-fly automata model checking starting from a first order representation of the system and a property automata.
• Read and understand theoretical descriptions of systems and algorithms and then transform those descriptions into real implementations.

Please see the Topics And Objectives for a detailed description.

None.

Modeling Checking by Edmund Clark, Orna Grumberg, and Doron A. Peled.

The book is available online through the Harold B. Lee library. To access, search for the book title on the library main page. It should be in the first few matches. Follow the Online link. This direct link should work on campus.

Principles of the SPIN Model Checker is an electronic book that covers the SPIN model checker and the PROMELA input language

The class meets TTh in 134 TMCB from 13:35h-14:50h for the Fall 2018. Lectures are one hour and fifteen minutes long. Class attendance is highly encouraged. Please see the detailed schedule for reading topics, due dates, exams, etc.

• Homework (70%)
• Midterm (15%)
• Final (15%)

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

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.

You will lose 10% for each day you are late for the first 7 days. After 7 days, handins are not accepted. Monday is the same as Sunday for counting late days. As such, a submission on Monday is the graded as if it were submitted on Sunday. Each student is given 3 free late days to use anytime in the semester for homework and projects (free late days cannot be used for exams). A free late day postpones the due date for the student by a single day. All homework and projects are due by midnight on the posted date.

The tests in this class are meant to require 2 hours of student time to complete. The schedule includes reading for each topic chosen to reflect topics of importance. The reading, quizzes, and homework are the basis for the tests.

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. If you miss an exam and cannot document a legal or medical emergency to justify it, then you can take the exam and receive up to 80% of its point value.

We encourage you to help one another in understanding the concepts, algorithms, or approaches needed to do the homework assignments for this class. However, what you turn in must be your own, or for group projects, your group's own work. Copying other people's code, solution sets, or from any other sources is strictly prohibited. Students in previous years have often been caught cheating by copying answers from the web, which turn out to be incorrect. The homework assignments must be the work of the students submitting the work.

The Honor Code includes a statement of standards regarding academic honesty. Academic honesty includes completing your own labs and tests unless there are express instructions to work in a group. Cheating in this class is sharing solutions to homework or tests either by copying, retyping, looking at, or supplying a copy in a file to someone else. Cheating is also leaving your solutions readable by other people on a shared file system or computer. The first violation of academic honesty standards will result in failing the class. All violations of academic honesty are documented and reported to the Honor Code office.

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.

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.