Week of Lectures Assignments

  1. Jan 18

  • Lecture: Course Overview
  • Lecture: Sets and Relations
  • Lecture: Isolette Example
  • Install: Alloy 5.1.0

  1. Jan 25

  • Lectures: Alloy Tour (a, b, c)

  1. Feb 1

  • Lectures: Alloy Tour (d, e)
  • Lecture: Introduction to AADL Component-based System Architecture

  • Project 1: Basic Alloy (due Feb 15)

  1. Feb 8

  • Lectures: Alloy Logic (b, c)

  1. Feb 15

  • Lectures: Alloy Logic (d, e)

  • Project 2: Advanced Alloy (due Mar 8)

  1. Feb 22

  • Exam: Alloy

  1. Mar 1

  • Install: Sireum IVE
  • Reading: End-to-End Formal Methods Integrated Development with SysMLv2 using HAMR
  • Reading: The Sireum Programming Language

  1. Mar 8

  • Lecture: HAMR Code Generation

  • Project 3: HAMR Code Generation (due Mar 29)

  1. Mar 15

  • Spring Break

  1. Mar 22

  • Lecture: HAMR GUMBO Contract

  1. Mar 29

  • Lecture: HAMR Code Generation for seL4

  • Project 4: HAMR GUMBO Contract (due Apr 12)

  1. Apr 5

  • Lecture: Introduction to Logika

  1. Apr 12

  • Lecture: Logika Basics

  • Project 5: Logika (due Apr 26)

  1. Apr 19

  • Lecture: HAMR+GUMBO and Logika

  1. Apr 26

  • Lecture: HAMR Testing Framework

  • Project 6: HAMR+GUMBO and Logika (due May 10)

  1. May 3

  • Lecture: Wrap-up

  1. May 10

  • No final exam