David Crocker’s Verification Blog

In case you missed the very interesting blog that David Crocker of Escher Technologies is writing since January of this year, I have put a link to it in the Blogroll that you find on the right of the Open-DO main page. David’s ArC system reads C code together with annotations written in special macros in order to formally prove properties of C code. Many similarities with Frama-C, yet a different interesting point of view. Plus David’s choice of examples and tone makes it a very nice reading.