Motivation How to build fully certified software systems? Source-level code + Libraries and runtime References with weak upd. Garbage collectors Dynamic mem.alloc. malloc()(strong update) Functions,exceptions,... Stacks,code pointers Concurrency Context switching Scheduler /0 Device driversMotivation How to build fully certified software systems? Source-level code + Libraries and runtime References with weak upd. Dynamic mem. alloc. Functions, exceptions, … Concurrency I/O Garbage collectors malloc() (strong update) Stacks, code pointers Context switching & Scheduler Device drivers