Archive

Archive for December, 2010

eCv beta 1 released!

December 20, 2010 2 comments

I’m pleased to announce that we’ve just released Escher C Verifier beta 1. We’re intending to keep the beta phase quite short, so barring major problems, full release of eCv should take place in January 2011. Read more…

Categories: C and C++ in critical systems

Verifying programs that use ‘sizeof’

December 12, 2010 Comments off

Consider the following code snippet (based on a real example of critical embedded software), whose purpose is to serialize some data and send it to another piece of hardware: Read more…

Categories: C and C++ in critical systems, Formal verification of C programs