Very recently I have been so lucky to have two papers accepted – on the same day even – at Formalise and AST respectively. They are both co-located with ICSE and both are in South Korea – fitting perfectly with my taekwondo :-). The conferences were supposed to be held in May, but has now been delayed until October due to the corona-virus. It was considered by the chairs whether it should be attempted to have a virtual conference. This was deemed impractical. Other conferences are opting for the virtual concept, and I start wondering whether virtual conferences become standard in the future.
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).
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.
Short story, I travelled to Oslo to meet up with my girlfriend, in order to attend the weeding of a friends of hers. Normally when talking about my travels, I usually end up talking about all of my travel trouble. Not this time though, as my travel went absolutely perfect. I did have some thoughts during my travel:
How easy it is to have your items stolen at security
A little backstory may be in order here. In Oslo my girlfriend had bought me a digital picture frame (thanks a lot), which I had put into my hand luggage. I had forgotten about it in security, thus when I took up all of my electronics on tray, I left that in my luggage. Naturally, I put my suitcase on another tray and my jacket on a third one. As luck would have it, my suitcase was taken out for inspection. As I was talking to the security officer, my electronics was down at the other end of the table. A thief could easily have snatched all of my electronics, and I could do nothing about it. I wonder if my insurance would actually cover theft from the airport.
As I am sure most air travellers have tried, airlines have priority boarding. I never quite understood that concept. The priority guests board first, but they are stuck in the aircraft until everyone else has boarded. They are not getting to their destination any quicker. A concept I would pay money for is “priority deboarding” – i.e. giving me priority in leaving the plane. The reason for this is, that I often have short trasnfers and I often want to catch a bus from Hamburg. A bus I always have to run for, because other passengers take too long in leaving the plane.
Quite some years ago, while I was writing my PhD-thesis I bought my first tablet. Not an expensive, but it was decent at the time. My plan was to use it for proof-reading my thesis on. Reading on a computer screen never really worked for me, so I always ended up printing material when proof reading. One could imagine how much paper I would end up using when proof-reading a thesis, so the tablet seemed like a good investment. Unfortunately, it never really panned out as a success because the flow of annotating the thesis with corrections on the tablet simply did not match the flow I had when reading with a paper and pen. I naturally kept my tablet and used it for other purposes and my paper usage continued. Until recently.
A New Attempt
As I had to proof-read an internal report for a project, and read bachelor students thesis several times, I once again realised how much paper I used. I again turned to my trusty tablet and tried replacing pen and paper with it. It did not work, but this time I refused to fail and decided that my tablet needed replacement – after all 5 years had passed and some progress must have been made on the tablet. To my horror the apparent best tablet – for my usage – is an ipad (yikes). Luckily, Samsung has an alternative – Samsung Galaxy TAB S4 – which I bought.
I have now had this tablet for approximately a month and quite happy with it. The big difference for me is, that it has a proper stylus making it possible to write notes by handwriting. That brings me much closer to a pen and paper workflow. I have one small annoyance with the tablet: it came with a styules, but the tablet itself has no holder for the stylus, so I had to buy an expensive cover for it from Samsung (which has the stylus holder).
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.
Last weekend I spend a long time writing a policy how we handle personal data
in Aalborg Taekwondo Klub. We required to make such a document due to
the new EU regulations.
I think it is good that companies and associations have to make such a
policy, and I think it is a very important subject EU has put focus
on. However, I fear it becomes a joke as people do not read the
policies and blindly accept them. Exactly as they do with EULAs.
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.
Spring has officially arrived and I have been eager to start skating again. Today I did it, I got home from work, picked up my skates and went out skating. I came to two relisations: 1) The streets are covered with an awful amount of sande, 2) It was really cold. I am not quite sure why the streets are sandy, but regarding 2) I know what went wrong. I did not dress properly. It had nothing to do with it being windy. I had just not dressed properly – cause as all danes know:
“There is no such thing as bad weather, only wrong clothing”.
As my friends will know, I am very involved with my old taekwondo club
in Aalborg. One “job” I have taken on me for the club is administering
our web-page soobak. In particular, setting up the web-page so
others can do the news updates (similar to this blog) so that I do not
have to do it everytime.
Yesterday and today, I spend quite some time modifying the existing
web-page to use a layout controlled by bootstrap. This has made it
responsive and thus much easier to use on mobile phones. Also, the
custom WordPress theme I originally made has also been made a bit
cusomisable – the slide show on the front page was not present
before and the text on the individual slides can be altered within
Although much of our internal traffic has moved to facebook nowadays,
I still consider it important to have a website that is easy to
administer and provides relevant information to people.
The current setup achieves this (I think).