Schedule of Topics (Tentative)

Additional resources.

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
10:00-noon!

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