Frama-C In about a month, on April 17 and 18, ANR the French research agency will hold a meeting on digital technologies. On this occasion ANR will also give 5 awards to projects it has funded in the previous years. It is my pleasure to announce here that U3CAT which has...
Read MoreWarning: on a punctiliousness scale ranging from zero to ten, this post is a good nine-and-a-half. There was no tag for that, so I tagged it both “C99” and “C11”. The faithful reader will know what to expect. There is a bit of C90, too. To summarize, it may appear...
Read MoreCRlibm is a high-quality library of floating-point elementary functions. We used it as reference a long time ago in this blog while looking at lesser elementary function implementations and the even lesser properties we could verify about them. A bold choice The CRlibm documentation contains this snippet: […] it may...
Read MoreIn a recent post, John Regehr reports on undefined behaviors in Coq! In Coq! Coq! Exclamation point! Coq is a proof assistant. It looks over your shoulder and tells you what remains to be done while you are elaborating a mathematical proof. Coq has been used to check that the...
Read MoreFrom Facebook to Silent Circle Some computers at Facebook were recently compromised because of a zero-day in Java. Nothing unexpected. Last december instead of writing a full blog post I lazily linked to Robert Graham predicting this sort of thing for the year 2013. Speaking of Facebook do you know...
Read More