analyzing relational logicDaniel Jackson, MITWG 2.3 · NewcastleApril 2000

language assumptions

analysis desired

analyses not possible

semantics: formulas

semantics: expressions

models

small scope hypothesis

example

what Alcoa does

scope monotonicity

every analysis is model finding

alcoa architecture

overview of method

SAT solvers

example

compositional translation

example

quantifiers

environments & trees

examples

compositional rules

symmetry

symmetry in boolean formula

symmetry constraint for a relation

generalizing symmetry

results

challenges

PPT Slide

PPT Slide

PPT Slide