Skip to main content
Link
Search
Menu
Expand
Document
(external link)
Formal Methods
Grading
Lectures
Set up Alloy Analyzer
Set up Dafny
Notes
Alloy Introduction
Constraint solving for Alloy
Dafny Introduction
Dafny and object orientation
Dafny invariants and arrays
Linear Temporal Logic
State Machines
Academia example
Readings
Resources
Readings
Class notes on modelling an
Academia setting in Alloy
Old class notes on modelling an
Academia setting in Alloy
Resources
Academy models for the Alloy Analyzer:
academia-1.als
,
academia-2.als
,
academia-3.als
,