Hacker Newsnew | past | comments | ask | show | jobs | submitlogin
A shallow survey of formal methods for C code (imperialviolet.org)
30 points by luu on Nov 10, 2014 | hide | past | favorite | 3 comments


Here's a link to an older thread for the same article, for convenience: https://news.ycombinator.com/item?id=8282949


For anyone interested, here is another paper concerning similar topics:

`Verification of a Cryptographic Primitive: SHA-256',

https://www.cs.princeton.edu/~appel/papers/verif-sha.pdf.

And don't forget about `CompCert C compiler',

http://compcert.inria.fr/compcert-C.html.

Or the `Vellvm' project,

http://www.cis.upenn.edu/~stevez/vellvm/.


His update to this old blog post is much better: https://www.imperialviolet.org/2014/09/11/moveprovers.html but he hasn't found cbmc yet.

A little list: http://anna.fi.muni.cz/yahoda/




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: