3 ms·
> The biggest programs ever verified "end-to-end" were ~10KLOC, or 1/5 the size of jQuery, and required years of work by world experts. Out of curiosity, what
by creata 6y ago
> The biggest programs ever verified "end-to-end" were ~10KLOC, or 1/5 the size of jQuery, and required years of work by world experts.
Out of curiosity, what programs are you referring to? seL4 seems to fit the description.
- pron 6y agoseL4 and CompCert are probably the biggest and they both correspond to under 10KLOC of C, i.e. they're very small by modern software standards (and not only are they small and still took years of efforts by experts, they had to be seriously simplified in order for the verification to be feasible). There have been much bigger programs verified with model-checkers (I vaguely recall seeing Samsung mention they model checked a 1MLOC Java program), but in those cases I think the properties were very specific.