Frama-C A coding contest of weeks past A fortnight ago, I sent an entry in this Quick Coding Contest. The objective of the contest is to produce a C function to convert a string to the integer it represents. Now it turns out that my submission generates the shortest code after...
Read MoreIn 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 More