FRAMES   NO FRAMES

# Course Description

## Overview

Formal methods are a methodology for the specification, analysis and verification of system behavior, both software and hardware. Specification is the process of describing a system and the functions it is expected to perform, whether before, during, or after its design. Analysis and verification use the specification of a system to confirm whether it satisfies its expected properties and/or determine conditions under which it does.

A formal-methods approach to specification, analysis, and verification, draws on mathematical (i.e., formal) logic and discrete mathematics, by viewing a system and its execution as mathematically-defined objects. Whenever applicable, a formal-methods approach 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 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 logical reasoning that will prepare them to use and profit from other formal methods in their studies beyond this course.

This session of the course (CS 512, Spring 2018) is the second part of a two-course sequence. The first part (CS 511, Fall 2017) was on the theory and applications of what are called SAT solvers and SMT solvers. This two-course sequence is justified because ideas and underlying logics of SAT/SMT solvers are a good preparation for topics we examine in this session of CS 512 (which vary from year to year in about 25% of the material), namely, the theory and applications of:

• model checking, based on material from the book [PMC], with a focus on linear-time logic (Chapter 5), computation-tree logic (Chapter 6), and probabilistic systems (Chapter 10),
• program verification, based on material from Chapter 4 in the book [LCS] as well as handouts, with a focus on Hoare Logic (HL) and some of its extensions: relational HL (RHL), probabilistic HL (pHL), and probabilistic relational HL (pRHL),
• verification of cryptographic proofs, using EasyCrypt,
• modal logics, based on material from the Chapter 5 and the end of Chapter 6 in the book [LCS] as well as handouts, with a focus on Kripke models and the mu-calculus.
The information on the books [PMC] and [LCS] is given later on this webpage.

# Prerequisites

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, extensive 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 10-12 take-home assignments, one mid-term exam and one end-of-term exam, and one term project. 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 Spring 2018 are interspersed as follows: 11 lectures, mid-term exam (85 minutes), 15 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.

# Lectures

Tue, Thu 11:00 am - 12:15 pm, in Room MCS B25.

# 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

# Exams

• MidTerm Exam: Thursday, March 1 ,   11:00 am - 12:15 pm,   Solutions
• EndOfTerm Exam: Tuesday, May 8 ,   12:30 pm - 2:30 pm,   Solutions

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.

# Term Projects

• Project Proposal: due Friday, February 3 (pdf file, at most one page, not graded)
• Term Project: due Thursday, May 4