3 ms·
As far as I understand, formal verification does not certify the implementation even though the algorithms used are sound.
by sudeepj 8y ago
As far as I understand, formal verification does not certify the implementation even though the algorithms used are sound.
- geofft 8y agoIt depends—many proof-assistant languages let you extract an implementation directly out of your formally-specified algorithm (generally by dropping rich typing-ish information, but you've already verified it's correct). Or take seL4, which amazingly proves that not just the C code but also the binary faithfully matches their formally-specified algorithms. https://sel4.systems/Info/FAQ/proof.pml https://sel4.systems/Info/FAQ/proof.pml Of course who knows what your CPU microcode is doing, but for the question at hand—ensuring a highly portable C library does what it claims to do more efficiently and accurately than exhaustive testing—formal verification is certainly a reasonable approach.