|
|
|
|
|
|
by oggy
5154 days ago
|
|
|
If you're interested, the German Verisoft project [1] aims at such pervasive verification. AFAIK they haven't yet verified anything matching the complexity of seL4, but they did verify a simple real-time OS. Of course you do need to stop somewhere, as in trusting something "blindly" (say, the verification tools themselves and the hardware they run on). [1] http://www.ertos.nicta.com.au/publications/papers/Klein_08.p... |
|
|