Department of Computer Science
CPSC 513: Introduction to Formal Verification and Analysis


Meets: MW 10:30-12:00pm. We're scheduled for ICCS 246, but we will start the first two weeks (through Sept 22) entirely on Zoom, due to some health concerns in my household. After that, we will re-evaluate, but we'll transition to in-person at some point (with the UBC-O students, and anyone else who wants to, still on Zoom).

First meeting is Monday, September 13!

Instructor: Alan Hu, CICSR 325, A J H at C S dot U B C dot C A

Links to Calendar, Readings, Assignments:

Reading List

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 Apple, Google, Amazon, Microsoft, IBM, Intel, AMD, 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:

There is no textbook for the course. Readings will come from the original research papers.

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.