High-assurance timing analysis for a high-assurance real-time operating system. | 1 | 0.35 | 2017 |
Finite Machine Word Library. | 0 | 0.34 | 2016 |
COGENT: Certified Compilation for a Functional Systems Language. | 1 | 0.36 | 2016 |
Refinement through restraint: bringing down the cost of verification. | 8 | 0.55 | 2016 |
A Framework For The Automatic Formal Verification Of Refinement From Cogent To C | 3 | 0.39 | 2016 |
Cogent: verifying high-assurance file system implementations | 19 | 0.74 | 2016 |
Comprehensive formal verification of an OS microkernel | 80 | 2.54 | 2014 |
Formally Verified System Initialisation. | 5 | 0.44 | 2013 |
Translation validation for a verified OS kernel | 41 | 1.26 | 2013 |
seL4 enforces integrity | 24 | 1.03 | 2011 |
Provable Security: how feasible is it? | 6 | 0.52 | 2011 |
Reconstruction of z3's bit-vector proofs in HOL4 and Isabelle/HOL | 15 | 0.64 | 2011 |
seL4: formal verification of an operating-system kernel | 84 | 5.86 | 2010 |
Mind the Gap | 0 | 0.34 | 2009 |
seL4: formal verification of an OS kernel | 584 | 19.89 | 2009 |
Secure Microkernels, State Monads and Scalable Refinement | 43 | 2.36 | 2008 |