Formal verification allows to find bugs in a program by systematically exploring all its feasible executions. I have used several formal verification tools during my PhD; since I feel there is a lack of technical blog posts about this topic on the Web, I’ll try and write some :)

This post deals with bounded model checking, specifically the CBMC tool and how to combine it with the Glucose solver. I believe this leads to a measurable increase in performance, at least when checking unsafe programs.

The tool paper that originated my previous post on demo videos got accepted. Hooray! Given the ongoing global pandemic, I was asked to submit a 15-minute video of my presentation, that has then been broadcasted to all participants. This post is a collection of notes I gathered along the way.

The Naming of Tools is a tough nail to hammer,
It isn’t just one of your parity games;
But I wonder why each and every programmer
always comes up with THE USUAL TWO NAMES.

This post will be part of a collection of notes about the way I currently deal with LaTeX documents. It is not a “for dummies” guide: some tools and extensions need a bit of configuration, and the user should already be familiar with LaTeX and some of its inner workings. I do feel that this setup allows an experienced user to become more productive in the long term, especially when dealing with a large document or with multiple documents at the same time.

Recently I had to produce a demo video as part of a tool paper submission. Here are some notes I gathered in the process: they might be useful to my future self or to other wannabe videomakers.

With the new year comes a new daily notebook! Since I always carry it around, I typically put a lot of personal data in the first pages of the notebook in the hope that, should I lose it somewhere, it will be found and returned. This time, as I was filling in the info page, I started thinking… Wouldn’t it be nice if I had some other way to prove that this thing is mine, without having to provide so much information? Some time ago I created an account on KeyBase and I used it to prove my identity over several websites. It is really a nice tool to experiment with PGP, so I recommend giving it a try.

Lately we needed to put a pair of small integers into a single int variable. (Let us gloss over the intricacies of what an int actually is and just assume it is 32-bit, shall we?) Nothing crazy hard but still, it took some trial and error before we got it right. So, if anybody needs it or is just curious, here’s the code:

The code will test all possible tuples and quit if some unpacking gives an unexpected result.