And also, we are seeing more and more certified C programs: see the DeepSpec NSF expedition grant, the Verified Software Toolchain, and the CertiKOS project for examples. I work with these guys.
You are soooo lucky. DeepSpec has a near dream team of people working on this issue. Appel and Chlipala alone could probably knock out most of the problem given enough time. Add the others and great stuff on publication list is entirely unsurprising. Except in its cleverness. :) Glad you brought it up as I haven't read the info flow for c & asm paper yet.
Btw, hows progress coming on those projects? Specifically, are any of the tools (a) useful for non-experts with a little bit of training by tutorials, etc and (b) available for download in open-source or binary form yet? Thanks ahead of time.
Btw, hows progress coming on those projects? Specifically, are any of the tools (a) useful for non-experts with a little bit of training by tutorials, etc and (b) available for download in open-source or binary form yet? Thanks ahead of time.