Course Description

Overview

Many time-tested and proven approaches to the design of robust and reliable software are based on formal methods. Formal methods provide a rigorous mathematical framework for the specification, analysis, and verification, of software properties. Specification is the process of formally 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. Approaches to software specification, analysis, and verification, based on formal methods draw on elements of mathematical logic as well as, depending on the application, other parts of mathematics called for by the latter. Whenever applicable, they lead to an increase in the reliability, robustness, and correctness, of a software system by several orders of magnitude.

However, ultimate success of these approaches in real-world applications largely 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. In this course and a follow-up course (CS 512), we therefore give special attention to approaches that are also amenable to automated implementation, encompassing different algorithmic methodologies for ascertaining that a software system satisfies its formally specified properties.

Among many such approaches and their automated implementations, this session of CS 511 (Fall 2019) focuses on the theory and practice of what are called SAT solvers and SMT solvers. This requires re-visiting elements of propositional logic and first-order logic from an algorithmic viewpoint, with a particular emphasis on tradeoffs between feasibility and expressibility (specifically: how to mitigate or circumvent complexity barriers in practice in order to be able to formally express and verify properties of software systems).

The material in this course is but only a small part (and one of the easier to learn) of the far broader area of formal methods, which now permeate many other 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. Lecture notes and homework assignments will include small applications from across computer science where problems of software analysis and verification arise which, though in principle solvable by hand, cannot be realistically solved without an automated SAT/SMT solver. We aim at providing students with enough fluency in formal reasoning and enough practice with a modern state-of-the-art SAT/SMT solver (Z3) that will stand them in good stead in studies beyond this course that call for the use of SAT/SMT solvers (or other automated logic-based tools, such as model checkers and interactive proof assistants, which often make extensive use of SAT/SMT solvers).

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.

Workload and Evaluation of Student Performance

Performance in the course is measured by a combination of 12 weekly take-home assignments, one mid-term exam, and one end-of-term exam. Six of the assignments consist of short problems to be solved by hand, and six of the assignments involve an implementation with the SAT/SMT solver Z3 together with the Python API (or front-end) for Z3, called Z3Py. (There are other SAT/SMT solvers and other API's for them, but only Z3 and Z3Py are allowed this semester.)

Full credit for each weekly assignment is based on solving 2/3 (or sometimes 3/4) of the problems; solving the remaining 1/3 (or 1/4) will add to the total credit for take-home assignments at the end of the semester. Final grades in the course will be computed based on the following percentages, approximately:

• about 50-55 percent for the 12 take-home assignments,
• and about 45-50 percent for the 2 exams.

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 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.

Logistics

Students and auditors from Boston University and nearby universities are all welcome.

Instructors: Assaf Kfoury, MCS 118, office hours on Tuesday and Thursday, 2:30 pm - 4:00 pm.

Meeting times and places: Lectures on Tuesday and Thursday, 12:30 pm - 1:45 pm, in Room MCS B29N. Lab Tutorials on Wednesday, 2:30 pm - 3:20 pm, in Room MCS B37N.

Online discussion: We will use Piazza for announcements, queries from students to the teaching staff, and queries between students. You will get an email from Piazza with a link inviting you to create an account within the first week of the Fall 2019 semester.

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.