3 ms·
CompCert There's now a lot of work in this space, e.g. http://sf.snu.ac.kr/sepcompcert http://sf.snu.ac.kr/sepcompcert and it's going to stay that way! Wh
by mafribe 11y ago
CompCert
There's now a lot of work in this space, e.g. http://sf.snu.ac.kr/sepcompcert http://sf.snu.ac.kr/sepcompcert
and it's going to stay that way!
Whoever said this has been proven wrong. This stuff works, it's just expensive. The only real question is: when will formal verification be convenient enough to be widely used in industry. I reckon that's 15-20 years away. Right now organisations like Facebook (http://fbinfer.com http://fbinfer.com) and Microsoft (https://www.fstar-lang.org https://www.fstar-lang.org) use it, but sparingly.
- cwzwarich 11y agoFacebook's Infer is just an ordinary static analysis tool, albeit one inspired by separation logic. It is unsound and does not prove that code is correct.
- mafribe 11y agoI agree, FB Infer is not a certifying compiler, but it's based on program logic.
- truncate 11y agoThe problem is most languages we use are not very safe, and which means if you have one unverified part in code, you can't prove code correct. I read a paper recently which tried to do modular verification of C by adding runtime contracts are boundaries[1]. Theory wise its sound, but it's really slow. You may even have to rewrite code certain ways to make it perform better. [1] https://lirias.kuleuven.be/bitstream/123456789/471365/3/sound-verification.pdf https://lirias.kuleuven.be/bitstream/123456789/471365/3/soun...
- nickpsecurity 11y agoEven more interesting from sepcompcert team: http://sf.snu.ac.kr/gil.hur/publications/ROSAEC_2014_002.pdf http://sf.snu.ac.kr/gil.hur/publications/ROSAEC_2014_002.pdf