Course Website: http://ece.uwaterloo.ca/~agurfink/ece750t29f18
LEARN: http://learn.uwaterloo.ca for assignments submissions and password protected course content
08:30-11:20AM Friday EIT-3151
Prof. Arie Gurfinkel, Office: DC 2522, first . last AT uwaterloo.ca, Office Hours: by appointment
TBD
No required textbook. Lecture slides, lecture notes, and reading material will be provided.
Computer systems are becoming smaller, faster, pervasive, ubiquitous, mobile, connected, adaptable, and “smart”. We are increasingly becoming more dependent on their correct operation. The border between safety-critical and non-safety-critical systems is being eroded. Dealing with complexity requires increased automation in development, testing, verification, and certification.
The dream of a mechanical verifier is as old as Computer Science itself. However, only in the last few decades have we seen a major breakthrough towards making it a reality. Starting with the adoption of Model Checking (a.k.a, Formal Verification) by the hardware semiconductor industry in the mid 90s, new techniques have emerged that combine decision procedures with novel heuristics to significantly automate software verification, testing, and certification.
The course will introduce students to the state-of-the-art research in automated verification. The course focuses on the recent advances in SAT and SMT-based automated verification techniques including: Conflict-Driven Clause-Learning (CDCL), Bounded Model Checking with SAT solvers, Unbounded Model Checking, Interpolation-based Model Checking, IC3, Property Directed Reachability (PDR), Software Model Checking, decision procedures for Constrained Horn Clauses, SMT-based Unbounded Model Checking, Predicate Abstraction, and Machine Learning-based Invariant Synthesis.
Students are expected to know the basics of First Order Logic (FOL) and Hoare Logic, and be able to program in Python and/or C++. Background in Compilers, Formal Methods, and Decision Procedures is useful, but is not required.
Grades may be curved or adjusted at instructor’s discretion.
All assignments will be returned in class, during office hours, or through LEARN.
By registering for this class, students agree to the following class policies:
Independent work. All work turned in will be that of the individual student unless stated otherwise. Violations would result in zero credit to all students concerned. Policy 71 will be followed for any discovered cases of plagiarism.
Lateness. You have 2 days of lateness to use on assignment submissions throughout the term. Each day you hand in an assignment late consumes one of the days of lateness. If you consume all of your late days, assignments that are still late will get 0 marks. You can only hand in an assignment up to the time all assignments are returned. Missed assignments get 0 marks. For example, you may hand in A1 two days late and A2 on time, or you can hand in A1 one day late and A2 one day late.
Academic Integrity. In order to maintain a culture of academic integrity, members of the University of Waterloo community are expected to promote honesty, trust, fairness, respect and responsibility. [Check http://www.uwaterloo.ca/academicintegrity for more information.]
Grievance. A student who believes that a decision affecting some aspect of his/her university life has been unfair or unreasonable may have grounds for initiating a grievance. Read Policy 70, Student Petitions and Grievances, Section 4, http://www.adm.uwaterloo.ca/infosec/Policies/policy70.htm. When in doubt please be certain to contact the departments administrative assistant who will provide further assistance.
Discipline. A student is expected to know what constitutes academic integrity [check http://www.uwaterloo.ca/academicintegrity] to avoid committing an academic offense, and to take responsibility for his/her actions. A student who is unsure whether an action constitutes an offense, or who needs help in learning how to avoid offenses (e.g., plagiarism, cheating) or about rules for group work/collaboration should seek guidance from the course instructor, academic advisor, or the undergraduate Associate Dean. For information on categories of offenses and types of penalties, students should refer to Policy 71, Student Discipline, http:://www.adm.uwaterloo.ca/infosec/Policies/policy71.htm. For typical penalties check Guidelines for the Assessment of Penalties, http://www.adm.uwaterloo.ca/infosec/guidelines/penaltyguidelines.htm.
Appeals. A decision made or penalty imposed under Policy 70 (Student Petitions and Grievances) (other than a petition) or Policy 71 (Student Discipline) may be appealed if there is a ground. A student who believes he/she has a ground for an appeal should refer to Policy 72 (Student Appeals) http://www.adm.uwaterloo.ca/infosec/Policies/policy72.htm.
Note for Students with Disabilities. The AccessAbility Services, located in Needles Hall, Room 1132, collaborates with all academic departments to arrange appropriate accommodations for students with disabilities without compromising the academic integrity of the curriculum. If you require academic accommodations to lessen the impact of your disability, please register with the AccessAbility Services at the beginning of each academic term.