Fall 2020

General Information


Instructor: Ronghui Gu ([email protected])

Office: 515 CSB

Office hours: Thu 13:00-14:00

TA: Xupeng Li ([email protected])

Office hours:

Mon 16:00-17:00, Tue 23:00-23:59

https://feline-hamster-182.notion.site/COMS-E6998-Formal-Verification-of-Systems-Software-Fall-2021-531e77f4166c4458b857df58476cb6ef

Coq Tutorial Lectures


The materials are borrowed from the Software Foundations textbook. If you are not familiar with Coq already, you should start by working on the following chapters ASAP. Make sure you actually do all of the exercises!

Coq Tutorial

TENTATIVE Syllabus (Subject to change!)

Syllabus

Lecture Notes

Lecture 1: Introduction

Lecture 2: Propositional Logic