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.
Continue »
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.
Continue »
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.
Continue »
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.
Continue »
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.
Continue »
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?
Continue »
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.
Continue »
