Final project presentations are Friday, December 13, from 1-4pm in ICCS 238. Final project reports due on Saturday, December 21. (More details, questions, etc. on Piazza or in class.)

• Meets: Tuesdays and Thursdays 2-3:20pm in ANGU 339.
  

  In recent years, I have taught this simultaneous/hybrid with live, in-person lectures livestreamed (with real-time questions, but also recorded) on Zoom. This was very convenient for students from UBC-O, or students who were traveling, etc. But it's also a sub-optimal compromise for both in-person and remote students. This year, I plan to start with the live/Zoom simulcast again, but if all students are physically in Vancouver and are OK switching to in-person only, I'm thinking of switching to in-person only. I plan to be masked during lectures, so even with a new COVID wave, I won't be aerosolizing viral particles at you during lecture.

• Zoom meeting ID for the lectures is: 698 8327 2461
  Passcode: 461130
  You should also be able to access this (and view lecture recordings) from Canvas.
  (If we end up with problems with security, I'll generate a new meeting for lectures, but given how many students are exploring courses right now, I'm going to keep things open.)
• Piazza Signup Link: piazza.com/ubc.ca/winterterm12024/cpsc513
  Piazza group for questions, informal chat, etc. I'll aim to check this regularly (and I often get overloaded with emails, so this gives an alternative way to reach me). It's also ideally a place for you all to hang out and help each other out.

First meeting is Tuesday, September 10! (Tuesday, September 3 has grad orientation activities, and it's usually too chaotic to start lectures in the first week, so no lecture on Thursday, September 5, either. However, I promise to be in my office ICCS 325 from 2-3:30pm (at least) on Thursday, September 5, so that will be a good time to find me if you have any questions/concerns about the class.)

Instructor: Alan Hu, CICSR 325,

Links to Calendar, Readings, Assignments:

Assignments

(Perpetually under construcction....)

Course Objectives:

Students completing the course will gain a solid foundation in current, practical formal verification techniques, the underlying theory, and significant experience applying these techniques to a real problem of the student's choosing. The course provides necessary background for advanced research in the field, as well as general exposure to this area for students pursuing research in other areas.

Introduction:

As computer scientists and engineers, we are building by far the most complex systems humans have ever created. And there is continuing demand for ever greater scale, features, performance, and complexity. The only way to build such systems is with computer assistance. And the only technique humans have to enable scalability is formalization.

Formal verification has been an integral part of computer science from the very beginning of the field, and there are seminal papers from the 1960s that are still influential today (which we might read). However, for a long time, the formal techniques lagged what could be accomplished via careful, but informal thought, trial-and-error, and a lot of hacking. Formal techniques were seen as an elegant approach to clarify thinking about programs or systems, but too cumbersome for real use. Even today, most undergraduate curricula pay little, if any, attention to formal techniques.

However, starting around the 1990s, the increasing scale of computer systems made informal approaches increasingly difficult, while at the same time, advances in formal algorithms and methodology, combined with increased computinng power, started to make formal verification and analysis techniques competitive, and sometimes superior or even indispensible, versus ad hoc approaches. One of the key ideas behind this revolution was an emphasis on highly automated verification techniques, with the emphasis on finding bugs faster, or finding the hard bugs, rather than trying to fully certify correctness.

The course is about the those automatic formal verification techniques, and their application to computer systems, be they hardware, software, or some combination. Although this isn't the trendiest or most well-known research area, the techniques have applicability to a wide range of other research areas, e.g., previous 513 students have found this course useful toward their thesis work in systems, security, AI, software engineering, FPGAs, architecture, etc. It's also a wonderful research area in itself, with substantial industrial demand for students with this training. I used to feel a little guilty about pushing my own research area, but as I travel, everyone (including people from cool places like Amazon, AMD, Apple, Google, Huawei, IBM, Intel, Microsoft, Nvidia, the major EDA companies, and several start-ups) is begging me for more verification students, and all of my grad students have landed great jobs. So, I don't feel guilty anymore. :-)

Textbook:

Prerequisites:

Graduate standing in CS or ECE, or consent of instructor. This area is a wonderful blend of theory, hardware, and software, but as a result, people's backgrounds will vary. I intend to make the course fairly self-contained, but familiarity with automata theory, mathematical logic, basic digital logic, differential equations, and some computer architecture will be helpful.