General Information

 

Objectives


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.

  • Basic predicate and temporal logics
  • Model checking (explicit-state -> Spin, symbolic -> SMV)
  • Model checking real-time systems (timed automata -> UPPAAL)
  • Decision procedures, such as SAT and SMT solvers (Yices)
  • Model synthesis and repair
  • Automated theorem proving (PVS)

Location and Time

Instructor: Borzoo Bonakdarpour, E5 4114, x31429,
URL: http://www.ece.uwaterloo.ca/~ece725
Lectures: Thu 8:30-11:20am, EIT 3151
Office Hours: Tue 11:30-12:30, Fri 11:30-12:30

Evaluation (preliminary)

Assignments 15%
Paper presentation 15%
Mid-term Exam 15%
Project - Report 30%
Project presentation- Oral exam      20%
In-class quizzes 5%

Lateness Policy

All homework assignments are due in the beginning of class (i.e., 8:30am). Submissions are made in teams of 2 students. You are allowed to submit one and only one assignment at most one week late. Other late submissions are subject to 50% deduction. All submissions must be typed unless they are electronic submissions (e.g., files, scripts, etc).

Academic Integrity

All students are expected to adhere to UW's academic integrity policies.