Paper Accepted at RP19

I recently had a paper accepted at RP19. I am very happy about this for a couple of reasons. Firstly, having a paper is always cool. Secondly, and maybe most importantly, this paper took a long time to finish, involved quite some programming – so it is nice to see that resulting in a accepted paper. Thirdly, it is my office mates first paper, so I am very happy on his behalf.

Enough talk about my happiness. The paper (arxiv version) is concerned with solving word equations. In particular, about solving a bounded fragment of word equations. As part of the paper we introduce the new tool Woorpje (hence the programming effort).

ETAPS 2019

Last week I attended ETAPS 2019, where I did a presentation at SPIOT19 (workshop on Workshop on Security practices for Internet of Things). That workshop was just a one-day event, but I took advantage of the situation and stuck around for the main conferences. Given my interests I mainly attended the TACAS conference. T


The week started with my presentation at SPIOT sunday. The workshop was fairly small. In fact, I believe there were only three accepted papers there, 1 invited talk and two talks by the organisers. It is the first time for me to attend such a small workshop, but I think it opened up for more engaging discussions during my presentation.


As already mentioned I attended the TACAS conference and naturally attended the keynotes of ETAPS. Before going to TACAS I had been wondering if the Boeing 737-Max incident would be brought up at the conference. The first keynote speaker (Marsha Chechik) brought it up approximately ten minutes into to her talk. Naturally just as an argument for why formal mehthods are needed. It was a very nice talk, though I will not talk about it in depth.

Another great talk was by Kathleen Fisher. She talked about using formal methods for asserting software do not have exploitable bugs – or rather she argued that it was the time for pushing formal methods into industry. Furthermore she discussed case studies where formal methods specialists had been involved with protecting a system (a quad-copter) from exploitable bugs. Another case study involved a UAV.


In the past week, I attended Federated Logic Conference in Oxford. A huge assembly of some of the most clever people within Logics and Software Verification. LICS and CAV was held as part of this assembly, and so was Formal Methods (FM) which I had an accepted paper at.


LICS is not really a conference I would normally attend, as it is a bit (just a bit :-p) more theoretical than what I do. However, since it was co-located with FM and CAV I decided to attend it. Peter O’Hearn gave a wonderful keynote about his work on integrating formal methods into the Facebook development cycle: he emphasized that the most important was to have tools run at diff-time – otherwise bugs found was not fixed. Another great talk was given by Karoliina Lehtinen, a colleague in Kiel, about parity games. I sure enjoyed it, and it seemed most others in the audience did as well.


The second half of the week, I attended CAV and FM. Byron Cook gave a fabulous talk about security in the Cloud at Amazon. Byron Cook also showed his media training worked, when he was asked about Amazons position in regards to meltdown and spectre: strangely enough he refused to comment on it.

At FM I had to present my own paper. I was a bit anxious (more than usual) before my presentation. Mainly because this was my first time to present Lodin at a conference. The presentation went quite well, and there was quite some discussions/questions afterwards.

Paper Accepted

Yay, I got my paper “Statistical Model Checking of LLVM Code” accepted for publication. The paper presents the tool, Lodin. A tool that performs both explicit-state model checking and Statistical model checking (SMC) of LLVM code. This combination of techniques is useful, since it allows applying SMC when the state space is too large for exhaustive techniques.

Statistical Model Checking is simulation-based and therefore it has a major drawback: finding rare events is very difficult for it. To help combat this, we integrated Lodin with Plasma-Lab. This integration provides access to Plasma-Labs many statistical methods among which is Importance Splitting. Importance splitting is exactly used for estimating probabilities of rare events.

The paper is joint work with Axel Legay, Dirk Nowotka and Louis-Marie Traonoues. A longer version of the paper is available here

The joy of flexible working hours

One of the nice things about my job as a post doc is my working hours: I can work whenever I want and whereever I want (with the small detail that I should come to the office once a day). This flexibility is nice since it allows me to leave early/come in late when I need to and adjust my working schedule to what fits me best. With the small caveat that we sometimes have morning meeetings with mandatory attendance!

However, the flexibility can also be a curse. I can work everywhere, making it very tempting to work when I have a free moment. In recent years I have discovered that my ability to relax is disappearing; instead I am constantly thinking of what work I have to do: writing that new publication we are planning to do, extend my tool with that feature (which would be nice for another publication). I always feel there is something I could be doing instead of sitting on the couch with a book or watching a movie.

This PhD-comics actually captures the situation perfectly.

enter image description here