Blog

Portable modulo signed arithmetic operations
Pascal Cuoq on 26 February 2013

In 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

From Facebook to Silent Circle, through the “metrics” Frama-C plug-in
Pascal Cuoq on 16 February 2013

From 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

ENSL seminar
Pascal Cuoq on 1 February 2013

Seminar As anticipated, I was at my alma mater's student seminar last tuesday. School and seminar were very much like I remembered them. The latter was improved by orange juice and biscuits to chat around after the talk, that I do not think were part of the protocol when I...

Read More

Customers, customers, customers
Pascal Cuoq on 24 January 2013

The recent posts on extremely minor undefined behaviors in zlib neatly tie in with a discussion on John Regehr's blog about the future-proofitude of C and C++. Another insightful post in this regard is this one by Derek Jones. Derek claims that the situation is different for proprietary compilers with...

Read More

2000s
Pascal Cuoq on 22 January 2013

Blogger of multiple qualities Harry McCracken was recently still looking for “an iPad PDF reader which can handle giant files which are 100s of pages long without choking”. Sorry I meant “STILL looking”. PDF is a nineteen-nineties technology to display text and pictures. Key quote: “Each PDF file encapsulates a...

Read More