Presentation outline
01 From specifications to proof goals
02 System models to symbolically executable models
03 Symbolic execution and relational property inference
04 6LoWPAN case-study