Weekly Schedule (Tentative)

 

We provide this schedule information to you to collect all lecture artifacts in one place, and to help you with your planning. We reserve the right to adjust this schedule based on the interest that the class shows in different topics, and based on travel schedules of the instructor.

 

The video lectures are linked directly from this page. If you have a slow internet connection it is always better to download the lecture first then view it. The audio/video quality will be poor otherwise.

 

Note: Some of the online lectures were recorded during previous course offerings. Once in a while you may hear/see a date/semester specific comment in the lectures (although we tried to avoid that). Please ignore all such references. The deadlines/procedures that apply this semester are the ones listed below and announced via e-mail and the lab session.

 

Week

Lecture

Reading

Lab

Assignment

1: Jan 20 - Jan 24

Lab: T

Course Administration
[
.pdf]

 

Course Overview

[.pdf, .mp4]

 

Sets and Relations
[
.pdf, .mp4]
(FYTD:
.pdf)

Hints to Specifiers, Jeannette Wing, July, 1995. [.pdf]

 

Formal Specification: a Roadmap, by Axel van Lamsweerde, in Future of Software Engineering (Limerick, Ireland). June, 2000. ACM Press. [.pdf]

 

 

 

 

 

2: Jan 27 - Jan 31

 

Lab: T

Alloy Tour (part a)

[.pdf, .mov, Flash]

 

Alloy Tour (part b)

[.pdf, .mp4, .als]

(FYTD: .als)

 

Allot Tour (part c)

[.pdf, .mp4, .als]

(FYTD: .als)

Jackson, Chapter 2

 

Exercises: Sets and Relations [.pdf]

 

Quiz #1: Overview and, Sets and Relations [solution: .txt]

 

 

 

3: Feb 3 - Feb 7

 

Lab: U

Alloy Tour (part d)

[.pdf, .mp4, 1.als, 2.als]

(FYTD: 1.als, 2.als)

 

Alloy Tour (part e)

[.pdf, .mp4, 1.als, 2.als]

(FYTD: 1.als, 2.als)

Jackson, Chapter 2

 

Exercises: Alloy Tour (parts a, b, c) [.pdf]

 

Quiz #2: Alloy Tour (parts a,b,c)
[solution:
.pdf]

 

 

4: Feb 10 - Feb 14

 

Lab: T

Alloy Logic (part b)

[.pdf, .mp4]

 

Alloy Logic (part c)

[.pdf, .mov, Flash]

Jackson, Chapter 3

 

 

Notes on Alloy Induction Concepts [.txt]

 

Quiz #3: Alloy Tour (parts d, e)

[solution: .pdf]

Homework #1

(due on Feb 24, 11:59pm)

[solution: .als]

5: Feb 17 - Feb 21

 

Lab: T

Alloy Logic (part d)

[.pdf, .mov, Flash]

(FYTD: .als)

 

Alloy Logic (part e)

[.pdf, .mov, .mp4]

(FYTD: 1.txt, 2.als, 2.txt)

 

Jackson, Chapter 3 & 4

 

Quiz #4: Alloy Logic (parts b, c)

[solution: .pdf]

 

6: Feb 24 - Feb 28

 

Lab: T

 

Introduction to UML/OCL

[.pdf, .mp4, 1.use, 2.use, 3.use]

 

OCL Basics

[.pdf, .mp4, 1.use, 2.use, 3.use, .cmd]

 

OCL Specification v1.5 [.pdf] and v2.2 [.pdf]

 

USE Documentation [.pdf]

Quiz #5: Alloy Logic (part d, e)

[solution: .pdf]

 

Homework #1 Review

 

Homework #2
(due on Mar 10, 11:59pm)

[solution: .zip]

7: Mar 3 - Mar 7

 

Lab: T

More OCL

[.pdf, .mp4, 4.use, 5.use, .cmd]

 

Advanced OCL Expressions

[.pdf, .mp4, 1.use, 1.cmd, 2.use, 2.cmd 7.use]

(see Week 6)

Quiz #6: OCL Basics

[solution: .pdf]

 

 

8: Mar 10 - Mar 14

 

Lab: T

 

 

(see Week 6)

Homework #2 Review

 

Quiz #7: Advanced OCL Expressions

[solution: .pdf]

 

A: Mar 17 - Mar 21

 

Spring Break

 

(see Week 6)

 

 

9: Mar 24 - Mar 28

 

Lab: T

Mining OCL Invariants from UML

[.pdf, .mp4]

 

Pre/Post-conditions in OCL and USE

[.pdf, .mp4, .use, .cmd]

(see Week 6)

Mid-term Exam

[solution: .pdf]

 

10: Mar 31 - Apr 4

 

Lab: T

 

(see Week 6)

Quiz #8: Advanced OCL and OCL Invariants

[solution: .pdf]

Homework #3

(due on Apr 18, 11:59pm)

[solution: .use]

11: Apr 7 - Apr 11

 

Lab: T

Design By Contract (DBC)

[.pdf, .mp4]

 

Spark Quick Tour

[.pdf, .mov]

Behavioral Interface Specification Languages, John Hatcliff, Gary T. Leavens, K. Rustan M. Leino, Peter MŸller, and Matthew Parkinson, ACM Computing Surveys, Vol. 44, No. 3, Article 16, Publication date: June 2012 [.pdf]

 

Spark Documentations

 

Spark Quick References:

  Quick Reference Guide 1 – Toolset and Annotations [.pdf]

  Quick Reference Guide 2 – Patterns [.pdf]

Mid-term Exam Review

 

Sireum Bakar Installation

[.mp4]

 

 

 

12: Apr 14 - Apr 18

 

Lab: T

Spark Functional Contract Notation

[.pdf, .mov]

(FYTD: 1.ada, 2.ada)

 

Bakar Kiasan

[.pdf, .mov, Standard.ada, Odometer.ada, Swap_Examples.ada, Simple_Sort.ada, .zip]

(FYTD: 1.ada, 2.ada, 3.ada)

(see week 11)

 

Bakar Kiasan: Flexible Contract Checking for Critical Systems Using Symbolic Execution, Jason Belt, John Hatcliff, Robby, Patrice Chalin, David Hardin, Xianghua Deng. NASA Formal Methods 2011: 58-72

[.pdf]

 

Enhancing spark's contract checking facilities using symbolic execution, Jason Belt, John Hatcliff, Robby, Patrice Chalin, David Hardin, Xianghua Deng. SIGAda 2011: 47-60

[.pdf]

Sireum Update

[.mp4]

 

Bakar Demo

[.mp4, .zip]

 

Bakar Exercise #1

[.zip]

 

13: Apr 21 - Apr 25

 

Lab: T

Introduction to JML

[.pdf, .mov]

 

Kiasan's Analysis (part a)

[.pdf, .mov]

 

KiasanŐs Analysis (part b)

[.pdf, .mov]

(see week 11)

 

JML Reference Manual

 

Towards A Case-Optimal Symbolic Execution Algorithm for Analyzing Strong Properties of Object-Oriented Programs, Xianghua Deng, Robby, John Hatcliff. SEFM 2007: 273-282

[.pdf]

Quiz #9: DBC, Spark, and Kiasan

[solution: .pdf]

Homework #4

(due on May 5, 11:59pm)

[solution: .ada]

14: Apr 28 - May 2

 

Lab: T

 

 

 

 

Quiz #10: KiasanŐs Analysis

[solution: .pdf]

 

15: May 5 - Dec 9

 

Lab: T

 

 

 

Review

 

16: May 12 - May 16

 

Final Week

 

 

Final Exam on May 13, 9:40am  - 11:30am