Course Description

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.

Prerequisites

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. 

Logistics

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.