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, 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 logic
  • Automated theorem proving (PVS)
  • Temporal logic (LTL and CTL)
  • Efficient state exploration techniques (explicit and symbolic)
  • Model checking tools (Spin and SMV)
  • Timed automata and model checking real-time systems (UPPAAL)
  • Decision procedures, such as SAT and SMT solvers
  • Software model checking: Predicate abstraction
  • Model synthesis and repair
  • Probabilistic verification (PRISM)
  • Runtime verification

Location and Time

Instructor: Borzoo Bonakdarpour, DC3331, x31851
URL: https://cs.uwaterloo.ca/~bbonakda/teaching/CS745
Lectures: Tue 4:00-6:50pm, DC 2568
Office Hours: Tue 10:00-11:00am, Thu 10:00-11:00am

Evaluation (preliminary)

Assignments 25%
Mid-term Exam 20%
Final Exam 20%
Project - Report 20%
Project presentation- Oral exam      15%

Lateness Policy

All homework assignments are due in the beginning of class (i.e., 4:00pm). Submissions should be made individually. 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.