Instructor: Stanley Bak

Email: Stanley.Bak@georgetown.edu

Remaining Due Dates

Oct 22 (at start of class) - HW 2

Oct 31 (end of day, 11:59pm) - Project Literature Review

Nov 5 (at start of class) - Research Paper presentation #1 - Matt

Nov 12 (at start of class) - Research Paper presentation #2 - Caleb

Nov 19 (at start of class) - Research Paper presentation #3 - Rahel

Nov 26 (end of day, 11:59pm) - Project Report Draft

Dec 3 - Project Presentation #1 - Rahel

Dec 3 - Project Presentation #2 - Caleb

Dec 5 - Project Presentation #3 - Matt

Dec 9 (end of day, 11:59pm) - Final Project Report

Useful Files

Syllabus

Course Project Tasks and Dates

Propositional / Predicate Logic Rules

Z3 and Z3py Demo Files

Homework

Homework 1 (Modified 9/16/2019. Due 9/24/2019 at the start of class. Code can be e-mailed to me.)

Homework 2 (Due 10/22/2019 at the start of class. Code should be e-mailed to me).

Lectures and Supplemental Readings

8/29/2019 Lecture 1 - Overview

Supplemental reading: https://www.seattletimes.com/business/boeing-aerospace/failed-certification-faa-missed-safety-issues-in-the-737-max-system-implicated-in-the-lion-air-crash/

9/3/2019 Lecture 2 - Propositional Logic

Supplemental reading: http://www-users.math.umn.edu/~arnold/disasters/ariane5rep.html

9/5/2019 Lecture 3 - Predicate Logic

Supplemental reading: https://cacm.acm.org/magazines/2017/8/219606-the-science-of-brute-force/fulltext

9/10/2019 Lecture 4 - Predicate Logic / SAT Tool Demo

9/12/2019 Lecture 5 - Hoare Logic

Supplemental reading: https://www.cs.cmu.edu/~crary/819-f09/Hoare69.pdf

9/17/2019 Lecture 6 - Hoare Logic, Part 2

9/19/2019 Lecture 7 - Abstract Interpretation

9/24/2019 Lecture 8 - Abstract Interpretation 2

HW1 Due!

9/26/2019 Lecture 9 - Predicate Abstraction and Lecture 9 - SAT

Supplemental Reading: Chaff: Engineering an Efficient SAT Solver

10/1/2019 Lecture 10 - SMT Solving

Supplemental Reading: De Moura, Leonardo, and Nikolaj Bjørner. "Satisfiability modulo theories: introduction and applications." Communications of the ACM

10/3/2019 Lecture 11 - Temporal Logic and Lecture 11 - Nelson Oppen

10/8/2019 Lecture 12 - Temporal Logic 2 and Model Checking Intro and Linear Temporal Logic

HW2 assigned

10/10/2019 Lecture 13 - Model Checking History and Computational Tree Logic

10/15/2019 Lecture 14 - CTL Examples - Computational Tree Logic

10/17/2019 Lecture 15 - Model Checking - Computational Tree Logic - LTL Model Checking

10/22/2019 Lecture 16 - LTL Model Checking

HW2 Due!

10/22/2019 Lecture 17 - Binary Decision Diagrams (BDDs) - BDD Operations

10/29/2019 Lecture 18 BDD and SAT Model Checking - BDD Operations

10/31/2019 Lecture 19 - Hybrid Automata - Timed Automata

11/5/2019 Lecture 20 - Reachability Analysis of Hybrid Automata

11/7/2019 Lecture 21 - Flowpipe Construction for Linear Systems - Logistics & HW

11/12/2019 Lecture 22 - Real-Time Systems Overview

HW Bonus Opportunity: Attend talk on Thursday, ask a question and hand in a 1-page summary for 25% bonus on last homework

11/14/2019 Lecture 23 - Real-Time Schedulability

Supplemental Reading: Liu, C. L., and Layland, J. W. "Scheduling algorithms for multiprogramming in a hard-real-time environment". Journal of the Association for Computing Machinery, 1973

11/19/2019 - Lecture 24 - Response Time Analysis

11/21/2019 - Special Lecture 25: Scalable Set-based Analysis for Verification of Cyber-Physical Systems (in Room 326, St. Mary's Hall)

11/26/2019 - Lecture 26: Scheduling Anomalies -Priority Inheritance Protocol (PIP) - Priority Ceiling Protocol (PCP)

12/3/2019 - Project Presentations (Rahel & Caleb)

12/5/2019 - Project Presentation (Matt)