Course Outline for CS745, Fall 2009

University of Waterloo

Course Number and Title: CS745, Computer-Aided Verification

Term and Year of Offering: Fall 2009

Section: 001
Lecture Time: Tue, Thu, 9-10:30
Room: MC 2034
Instructor: Nancy Day, DC2335, nday@cs.uwaterloo.ca
Office Hours: TBA

Course Description:

This course introduces the theory and practice of computer-aided verification for the design and analysis of digital systems (i.e., hardware and software systems). It emphasizes formal methods techniques, i.e., techniques based on logical reasoning and mathematical modelling, which are gradually being incorporated into CASE and CAD tools. These techniques have been used to find subtle, critical logic and safety errors in industrial hardware and software systems.

Course Objectives:

To introduce the fundamental concepts of formal methods.
To introduce the range of topics within formal methods and to provide a map to guide the student towards future research in this area.
To provide hands-on experience with formal methods tools. FM is an area that combines both theory and practise.
To learn what research is and how to do it.

Course Overview:

Theory and Modelling (10 hrs)
Algebraic and logical preliminaries: partial orders, lattices, lambda-calculus. Classical logic. Automata. Formal modelling and specification.
Temporal Logic and Model Checking (8 hours)
Linear and branching-time temporal logic. Explicit state and symbolic state model checking. State space reduction. Abstraction. Compositional reasoning.
Decision Procedures (5 hours)
Decision procedures for propositional logic. Decidable subsets of first-order logic.
Mechanized theorem proving (5 hours)
Interactive proof. Automated reasoning. Combining proof tools.
Advanced Topics (8 hours)
Chosen by the instructor. e.g., Invariant generation, Infinite state systems, Non-classical logics, Abstract interpretation.

Prerequisites:

Undergraduate knowledge of logic and discrete math (propositional and predicate logic).

Required text:

None. Lecture notes provided on-line.

Late policy:

No late assignments will be accepted.

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 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, www.adm.uwaterloo.ca/infosec/Policies/policy70.htm. When in doubt please be certain to contact the department's administrative assistant who will provide further assistance.

Discipline: A student is expected to know what constitutes academic integrity [check www.uwaterloo.ca/academicintegrity/] to avoid committing an academic offence, and to take responsibility for his/her actions. A student who is unsure whether an action constitutes an offence, or who needs help in learning how to avoid offences (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 offences and types of penalties, students should refer to Policy 71, Student Discipline, www.adm.uwaterloo.ca/infosec/Policies/policy71.htm. For typical penalties check Guidelines for the Assessment of Penalties, 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) www.adm.uwaterloo.ca/infosec/Policies/policy72.htm.

Note for Students with Disabilities: The Office for persons with Disabilities (OPD), 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 OPD at the beginning of each academic term.