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 propositional logic and first-order 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 mostly focused on -- but not entirely limited to -- the theory and practice of specific state-of-the-art proof assistants (also called interactive theorem provers) and their uses in automated reasoning, in formal verification, and more generally, in solving challenging mathematically formulated problems.
The preceding material, both the background theory and its implementation in automated formal tools, is covered in approximately 75-80 percent of the course. The remaining approximate 20-25 percent is devoted to a deeper examination of different topics in mathematical logic, which may vary from one iteration of the course to the next. This 20-25 percent depends on students' interests in consultation with the instructor, and typically permeates all parts of the course, though mostly covered towards the end of the semester. For example, in past iterations, this 20-25 percent of the course focused on intuitionistic logic and more broadly constructive logic, or focused on higher-order logic and more broadly type theory. In Fall 2025, this part of the course will focus on elements of model theory.
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 2025), we will use the more recently developed Lean proof assistant (which doubles as a programming language Lean).
Lean is a 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 proof assistants 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).
Students are allowed to omit the Lean 4 problems in the weekly assignments provided they do a semester-long project on a Lean 4 related topic, discussed and approved by the instructor.
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.
Students and auditors from Boston University and nearby universities in the Boston area are all welcome.
Instructor: Assaf Kfoury, CDS Room 1011. Office hours: TBA.
Teaching Fellow: TBA.
Meeting times and places: Lecture on Tuesday and Thursday 2:00-3:15 pm, Laboratory on Wednesday 12:20-1:10 pm. All lectures and all lab sessions are in Room CDS 801.
Academic calendar for Fall 2025: click here.
Online discussion: We will use Piazza for announcements, queries from students to the teaching staff, and queries between students.
Please read carefully Boston University's policies on academic conduct:
Instructors are required to strictly enforce these policies.