A formal-methods approach to specification, analysis, and verification, 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 2017) is the first part of a two-semester sequence: The first part (this semester) is on the background, theory, and applications, of what are called SAT solvers and SMT solvers. The second part in a follow-up semester (Spring 2018) will be on the background, theory, and applications, of model checking and automated model checkers. This two-part sequence is justified because many ideas and underlying logics of SAT/SMT solvers extend naturally to ideas and underlying logics of model checking; an in-depth examination of the former is a good preparation for an in-depth examination of the latter.
Performance in the course is measured by a combination of 11 (or 12) take-home assignments and two in-class exams. To master the conceptual material covered 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 2017 are interspersed as follows: 15 lectures, mid-term exam (85 minutes), 11 lectures, end-of-term exam (120 minutes).
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 "Incomplete" grades in this course.
Wed 10:10 am -11:00 am in Room MCS
Wed 2:30 pm -3:20 pm in Room MCS B25.
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: Tue 1:00 pm - 2: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.