4 ms·

Interesting work. I don't remember who said that "formal verification is the way of the future... and it's going to stay that way!" Quite strange that the arti

by hbbio 11y ago

Interesting work. I don't remember who said that "formal verification is the way of the future... and it's going to stay that way!" Quite strange that the article doesn't mention CompCert though, which has an extensive bibliography: http://compcert.inria.fr/publi.html http://compcert.inria.fr/publi.html Edit: The person I quote is a researcher in formal verification, I think it's Gérard Huet from Inria.

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 ago
  Facebook'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 ago
    I agree, FB Infer is not a certifying compiler, but it's based on program logic.
- truncate 11y ago
  The 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 ago
  Even 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

by hbbio 11y ago

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 ago
Facebook'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 ago
  I agree, FB Infer is not a certifying compiler, but it's based on program logic.
truncate 11y ago
The 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 ago
Even 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