3 ms·
Plus Frama-C, model-checkers, concurrency analyzer, CompCert in Coq, Simpl in HOL, symbolic execution in KLEE, path-based testing, and property-based... then it
by nickpsecurity 9y ago
Plus Frama-C, model-checkers, concurrency analyzer, CompCert in Coq, Simpl in HOL, symbolic execution in KLEE, path-based testing, and property-based... then it might be good to go.
On a capability-secure processor running in a VM in case new classes of attack against C code are discovered
Again. ;)