| Date | Topic | Readings/Topic | Lecture | Homework |
|---|---|---|---|---|
| Wed Aug 27 | Introduction | 01_intro.pdf | ||
| Wed Sep 03 | Predicate Logic | No Silver Bullet Paper | 02_FOL_1 |
HW #1 Due: Sep 15 |
| Mon Sep 08 | Predicate Logic | Continued 02_FOL Worksheet |
||
| Wed Sep 10 | Predicate Logic | 03_FOL_2 | ||
| Mon Sep 15 | Predicate Logic | Continued | HW #2
Due Sep 22 |
|
| Wed Sep 17 | Alloy | Jackson § 1 & § 2 | 04_alloy_intro | |
| Mon Sep 22 | Alloy | Jackson § 3 Tutorial, Chapter 1 |
05_alloy_logic_in_class.pdf | |
| Wed Sep 24 | Alloy | Jackson § 4 Tutorial, Chapter 2 |
06_alloy_langugage_analysis.pdf | HW #3 Due Oct 1 |
| Mon Sep 29 | Alloy | Jackson § 5 Tutorial, Chapter 3 |
07_AddressBookExamples | |
| Wed Oct 01 | Alloy |
08_alloy_hotel_locking.pdf
08_HotelLocking |
||
| Mon Oct 06 | Alloy/SPARK | An Introduction to Design-By-Contract | Finish up Hotel Locking SPARK Tutorial |
Install SPARK Toolkit |
| Wed Oct 08 | NO CLASS | Work through the SPARK Tutorial | HW #4 | |
| Mon Oct 13 | SPARK | Overview of Ada & SPARK | 09_spark_intro.pdf | |
| Wed Oct 15 | SPARK | Flow Annotations & Analysis | 10_spark-ifa.pdf | |
| Mon Oct 20 | SPARK | Continued (ifa) | ||
| Wed Oct 22 | SPARK | Basic Functional Contracts | 11_spark_contracts.pdf | |
| Mon Oct 27 | SPARK | Generating Proof Obligations | 12_spark-vcs.pdf |
HW #5
Due: Nov 3 StackPackageHW1.zip |
| Wed Oct 29 | SPARK | Continued (vcs) | ||
| Mon Nov 03 | SPARK | Continued (vcs) | ||
| Wed Nov 05 | SPARK | Abstraction and Refinement | 13_spark-refinement.pdf | HW #6: Due: Nov 12 ExchangeSortHW6.zip IsqrtPackageHW6.zip FindHW6.zip |
| Mon Nov 10 | LTL | Temporal Logic (11.1-11.3) | 14_introLTL.pdf | DUE: Term Paper Proposal |
| Wed Nov 12 | LTL | Simple On-the-fly Automatic Verification of Linear Temporal Logic |
Sick day | HW # 7: Due Nov 19 exerciseLTL_1.pdf |
| Mon Nov 17 | RESEARCH | |||
| Wed Nov 19 | RESEARCH | |||
| Mon Nov 24 | LTL | (See Nov 12) | 15_LTLSemanticTableau.pdf | |
| Wed Nov 26 | CTL | Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications |
16_introCTL.pdf
17_CTLexplicitStateMCalgo.pdf |
|
| Mon Dec 01 | Presentations | 1) Spec # | David: Spec # Presentation | DUE: Term Paper |
| Wed Dec 03 | Presentations | 2) An Analysis of TLA+ 3) Probabilistic Model Checking |
Kevin: TLA+ Presentation
Mohammad: Probabalistic MC Presentation |
|
|
Thu Dec 11
|
Presentations | 4) Correctness of Model Transformations 5) Stochastic Local Search Techniques for Theorem Provers 6) Frama C |
Matt: On the Correctness of Model Transformations
Khaled: Stochastic Local Search Techniques for Theorem Provers Ben:Frama C |