Outline of This Talk Motivations and contributions SCAP logic for verifying function call/return 。Basic framework ■Specifications ■Stack-invariant Instruction rules(to enforce the invariant) Generalizations for complicated controls Implementation applicationsOutline of This Talk ◼ Motivations and contributions ◼ SCAP logic for verifying function call/return ◼ Basic framework ◼ Specifications ◼ Stack-invariant ◼ Instruction rules (to enforce the invariant) ◼ Generalizations for complicated controls ◼ Implementation & applications