CpSc 513: Introduction to Formal Verification and Analysis

Overview

Formal verification and analysis started as the application of rigorous mathematical methods to show that hardware and software designs have the desired properties. Verification remains a major part of formal methods: every large chip design project has a formal verification team to prevent costly errors from making it through fabrication. In the past 10 years, formal methods have been rapidly growing in supporting software development. More recently, formal methods are finding application in areas beyond finding bugs. Interest in software synthesis is growing with applications such as Excel™'s FlashFill enabling non-programmers to create useful Excel macros. Efficient solvers for SAT (boolean satisfiability) and SMT (Satisfiability Modulo Theories, i.e. SAT plus decision procedures for arrays, lists, other data structures, linear programs, non-linear inequalities ...) have found application in optimization methods (and vice-versa). For example, MonoSAT (developed by Sam Bayless, Alan Hu, and Holger Hoos at UBC) is used by Amazon for AWS resource provisioning and security checks.

Is CpSc 513 for you? Of course! ☺ I assume that you've never had a formal methods course before -- now is a great time to get acquainted. The methods and applications of formal methods cover a wide range of computer science including theory, systems, programming languages, concurrency, AI, and robotics. If you are interested in multiple areas of computer science, you'll do well in your career, and you'll have fun in CpSc 513.

Specifics

• Lectures: Tuesday/Thursday, ICCS 246, 3:30-5:00pm
• First lecture: January 7, 2020 (Term 2)
• Instructor: Mark Greenstreet, ICCS 323
• Reading list: Feel free to drop by my office or send me e-mail to let me if there are topics that you would like included. The reading lists from ealier years can be handy if your looking for related papers:
  • 2016 reading list (i.e. the last time I taught it)
  • 2018 reading list (when Alan Hu taught CpSc 513 last year).
  Recognizing that formal methods is new to everyone, I plan to cover roughly one paper per lecture. Each student is expected to present a paper in class. I want to add some recent papers on software verification, software synthesis (e.g. Rosette), AI methods for theorem proving, and some recent work in robotics (I see that was missing from Alan's reading list). Of course, this means I'll have to figure out what to cut. Formal methods is a fast growing field, and we can no longer cover the whole field in one term.
• Homework: I intend to have four assignments where you will try examples with different tools such as a BDD (symbolic boolean) package, Z3 (a state-of-the-art SMT solver), and other tools.
• Project: I'll define the details as the course continues. The goal of your project is to produce a master's thesis proposal. To get more details, click here.