tractable object modelsDaniel JacksonSoftware Design GroupMIT Laboratory for Computer ScienceWG 2.9 · Flims · February 7, 2000
lightweight formal methods
progress
semantic minimalism
relational structure
example
modelling implication
partial function problem
my approach
an example
basic notions
object model diagram
Alloy model: declarations
an indicative invariant
a safety condition
two definitions
policy invariants
an operation
analysis strategy
bug example, inconsistency
bug example, implication
output
bug example, preservation of invariant
funky overlap
why it’s hard (1)
small scope hypothesis
why it’s hard (2)
translating to SAT
research status
conclusion