Week of Lectures/Assignments

  1. Jan 18

  • Course Overview
  • Sets and Relations
  • Install: Alloy 5.1.0

  1. Jan 25

  • Alloy Tour (a, b, c)

  1. Feb 1

  • Alloy Tour (d, e)
  • Project 1: Basic Alloy (due Feb 15)

  1. Feb 8

  • Alloy Logic (b, c)

  1. Feb 15

  • Alloy Logic (d, e)
  • Project 2: Advanced Alloy (due Mar 8)

  1. Feb 22

  • Exam: Alloy

  1. Mar 1

  • Introduction to SysMLv2 and HAMR
  • Install: Sireum IVE

  1. Mar 8

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

  1. Mar 15

  • Spring Break

  1. Mar 22

  • HAMR GUMBO Contract

  1. Mar 29

  • HAMR Code Generation for seL4
  • Project 4: HAMR GUMBO Contract (due Apr 12)

  1. Apr 5

  • Introduction to Logika

  1. Apr 12

  • Logika Basics
  • Project 5: Logika (due Apr 26)

  1. Apr 19

  • HAMR+GUMBO and Logika

  1. Apr 26

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

  1. May 3

  • Wrap-up

  1. May 10

  • No final exam