Frama-C If Frama-C doesn't work out, we can always make a comedy team Facetious colleagues ask me how I make Frama-C's value analysis' messages so informative. \Pascal " one of them says "in this case study the generated log contains 8GiB of information! It won't open in Emacs...". I helpfully point...
Read MoreI have been able to divert a few hours yesterday and today for programming. It was well worth it, as I have discovered a theorem. It is new to me, and I wonder whether it was ever published. The theorem is, a C program cannot double free() a block even...
Read MoreJustification There recently was a thread in the Frama-C mailing list on verifying the Rijndael cipher, standardized and better-known as AES. Nowadays, AES is mostly famous for being sensitive to timing attacks. An attacker measuring the time it takes to encrypt known plaintext with an unknown key can deduce the...
Read MoreIn 2011, I got an Xbox 360. It's not what I would have liked but you know what they say about not looking gift consoles in the mouth especially when you get them one solstice early. When in the game shop I saw in the second-hand games bin the game...
Read MoreI would use a social network where the discussions are about the near future's zeitgeist. As they are, people just use them to discuss what is happening now (\what are you doing?") which does not have the same usefulness. Case in point: Christmas just came and went; presents given and...
Read More