Course Description


A proven approach to the design of robust and reliable software involves formal methods. Formal methods are a rigorous mathematically-based means to specify, analyze, and verify software behavior. Specification is the process of describing a software system, the functions it is expected to perform and the outputs it is supposed to return. Analysis and verification use the specification to confirm whether the software system satisfies its expected properties and/or determine conditions under which it does. A formal-methods approach to specification, analysis, and verification, primarily draws on mathematical (i.e., formal) logic and discrete mathematics. Whenever applicable, it leads to an increase in the reliability, robustness, and correctness, of a system by several orders of magnitude.

In this course, special attention is given to formal approaches that are amenable to automated or semi-automated verification, encompassing different algorithmic methodologies for ascertaining that a software system satisfies its formally specified properties. Success of formal methods in real-world applications depends on their being automated, partially or fully, and on their scaling up to large systems beyond the ability of human agents to analyze and verify by hand.

We aim at introducing students to some of the formal methods most encountered in computer science, but also at providing them with enough fluency in formal-logic reasoning that will prepare them to use and profit from other formal methods in their studies beyond this course.

This session of the course (Fall 2018) is the first of a two-semester sequence: The first (this semester) is on the theory and practice of what are called SAT solvers and SMT solvers, which includes re-visiting elements of propositional logic and first-order logic from an algorithmic viewpoint and examining tradeoffs between feasibility and expressibility (specifically: how to mitigate or circumvent complexity barriers in practice in order to be able to formally express additional properties). The second follow-up semester (Spring 2019) will be divided into two parts: (1) an introduction to the temporal and modal logics underlying model checking and the use of automated model checkers, and (2) program verification based on three extensions of Hoare Logic (HL) -- relational HL, probabilistic HL, and probabilistic relational HL -- which is necessary background to understand verification of cryptographic proofs using the system EasyCrypt.

This two-semester sequence is justified because many ideas and underlying logics of SAT/SMT solvers extend naturally to ideas and underlying logics of model checking and program verification; an in-depth examination of the former is a good preparation for an in-depth examination of the latter.


There is one formal course prerequisite: CS 320, or CS 330, or CS 350, 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 (in the numbering of the Boston University Course Bulletin). Moreover, programming experience with at least one high-level programming language is essential.

Workload and evaluation of student performance

Performance in the course is measured by a combination of 11 (or 12) take-home assignments, one mid-term exam, and one end-of-term exam. Every take-home assignment has two parts: the first part consists of short exercises to be solved by hand, the second part is an implementation involving Z3 (a current state-of-the-art SAT/SMT solver) for which students can choose one of two API's to facilitate interaction with Z3: the Python API for Z3 (click here) or the OCaml API for Z3 (click here and here). There are other API's for Z3, but these two are the only allowed this semester.

To master the conceptual material presented in lecture and in reading assignments, students should spend the time and energy normally expected for a 4-credit 500-level course, which means an average of between 10 and 15 hours per week (including attendance of two 75-minute weekly lectures) over a 14-week semester. Lectures and exams in Fall 2018 are interspersed as follows: 15 lectures, mid-term exam, 11 lectures, end-of-term exam.

No late policy. This is a fast-pace course. Solutions for take-home assignments are posted shortly after their deadline. In the event of serious illness, make-up examinations will be given orally. There are no "I" ("incomplete") grades in this course.

Lectures and Tutorials

Lectures --
       Tue, Thu 12:30 pm - 1:45 pm, in Room MCS B25.

Tutorials --
       Wed 2:30 pm - 3:20 pm in Room MCS B21 B31,
       Wed 3:35 pm - 4:25 pm in Room CAS 221.

Teaching staff

Instructor -- Assaf Kfoury
       Office Hours: Tue 2:30 pm - 4:00 pm, Thu 2:30 pm - 4:00 pm
       Location: MCS 201 C, e-mail: kfoury at bu dot edu

Teaching Assistant -- Tomislav Petrovic
       Office Hours: Mon 2:00 pm - 3:30 pm, Wed 1:00 pm - 2:30 pm
       Location: PSY 225, e-mail: tomislav at bu dot edu


The exams are closed book. You may, however, bring one 8.5 by 11 sheet of paper (i.e. one regular-size sheet of paper) as a crib sheet. Preparing a crib sheet can be a useful study aid, so take time in selecting material for it. You may use both sides of the paper and write as small as you like, but in any case, you are allowed only one sheet.  

Books and reading material

Mailing list

For online discussions, we will use Piazza. Click here to sign up (or to login, if you already have a Piazza account). Use Piazza for queries, from enrolled students to instructors, as well as for queries between enrolled students.

Other courses to fulfill software requirements

Maintained by Assaf Kfoury
Created: 2018.08.01    Last modified: 2018.09.11