Lecture notes, slides, and reading material are located at the Lectures & Reading Material page.
Homework and additional resources are located at the Homework & Additional Resources page.
Overview
The material in this course covers but a small part of what are commonly called formal methods in computer science. Even though our coverage starts from the most basic notions of logic, familiar to most upper-level undergraduate and graduate students, it quickly develops to the level required for an understanding of how formal methods have permeated many areas of computer science, notably areas that depend on the development of safety-critical and/or security-critical software systems -- systems that must be guarded against accidental malfunctions and/or malicious interference. The underlying foundation of formal methods in computer science is a well-established area of mathematics, mathematical logic; put differently, formal methods can be viewed as applications of mathematical logic to computer science. This is material that is essential for understanding the principles of automated reasoning and its various subareas, and how they can be used to solve problems of computer science (and, in fact, problems of other mathematically based disciplines) and, in particular, to construct provably-safe and provably-secure software systems.
There is currently available an enormous variety of automated formal tools and formal development environments -- such as model checkers, SAT solvers, SMT solvers, verification-aware programming languages, dependently typed functional languages, among several other categories, each with its own foundation from a different part of mathematical logic, its own preferred methodology, and its own intended target problems -- which can be used to accomplish the goals described in the preceding paragraph and to test their usefulness in practice. This is a very broad collection of software artifacts, whose mere survey is already well beyond the limits of a single one-semester course. The scope of CS 511 is far narrower, as it is focused on the theory and practice of specific state-of-the-art automated theorem provers (ATP's) and interactive proof assistants (IPA's) -- with an emphasis on one or the other in different years -- and their uses in automated reasoning, in formal verification, and more generally, in solving challenging mathematically formulated problems.
In past iterations of this course, we used the Coq proof assistant, the Isabelle proof assistant, and the SAT/SMT solver (a special form of theorem proving) called Z3 -- each in a different year. In this iteration of CS 511 (Fall 2023), we will use the more recently developed Lean proof assistant.
Lean is a complex and powerful system, one of the better (and friendlier!) interactive proof assistants currently available. We will use the fourth version of the system, called Lean 4, and we will use it in a fairly limited way in fact, mostly to demonstrate the potential of IPA's in tackling problems that are in principle computationally feasible, but unavoidably tedious and error-prone, when solved rigorously and precisely by hand.
There is one formal course prerequisite: CS 320, or CS 330, or CS 350 (in the Boston University Course Bulletin), or the instructor's permission. However, to succeed in this course and make the best of its intellectual contents, students should have the preparation and maturity acquired by successfully completing all required computer science courses up to at least 300-level. Moreover, programming experience with at least one high-level programming language is essential.
Performance in the course is measured by 14 weekly take-home assignments. There will be no mid-term exam and no end-of-term exam in this course. Every take-home assignment will have two parts: problems to be solved by hand (typed and submitted in PDF format) and problems to be solved with Lean 4 (coded as Lean 4 scripts).
To master the material presented in lecture, homework, and reading assignments, students should expect to spend the time and energy normally required by a 4-credit 500-level graduate course, which means an average of between 10 and 15 hours per week (including attendance of two 75-minute weekly lectures and one 50-minute weekly lab) over a 14-week semester.
For an approximation of the topics we will cover in Fall 2023, you may want to consult the course website for Fall 2021.
Students and auditors from Boston University and nearby universities are all welcome.
Instructor: Assaf Kfoury, CCDS Room 1011. Office hours: Tuesday 2:00 pm - 3:30 pm, Wednesday 4:00 pm - 5:30 pm.
Teaching Fellow: Aaron Letizia, CCDS 1002. Office hours: Wednesday 12:30 pm - 2:00 pm, Thursday 3:30 pm-5:00 pm.
Meeting times and places: Lectures on Tuesday and Thursday, 9:30 - 10:45 am in EPC 208. Lab Tutorials on Wednesday, 2:30 pm - 3:20 pm in CAS 229.
Online discussion: We will use Piazza for announcements, queries from students to the teaching staff, and queries between students.
No late policy: This is a fast-pace course. Selected solutions for take-home assignments are posted shortly after their deadline. There are no "I" ("incomplete") grades in this course.
Please read carefully Boston University's policies on academic conduct:
Instructors are required to strictly enforce these policies.