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.
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
I have been writing a lot of Latex code lately, and thought I would write about my Latex setup.
Continue reading “Writing Papers with LaTex”
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.