trust

Freek Wiedijk Radboud University Nijmegen

3SWeb project meeting MLstate, Paris

2009 10 19

binary compiler source algorithm interface

formalization

VC generation extraction proof assistant

runtime

processor disk operating system file system