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.
The paper is joint work with Axel Legay, Dirk Nowotka and Louis-Marie Traonoues. A longer version of the paper is available here
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).
At the moment I’m working on a few papers. One of them is a rewrite of
a recently rejected paper (that’s life right?) and the other a brand
For both of the above mentioned papers I am naturally using LaTex for
text processing and a version control system – git. I am big fan of
git – well any version control actually. The number of times I have
been saved by version control is uncountable by now. However, there are two things version control has never protected me from: forgetting to
add a file to my repository or forgetting to push to the
repository. In fact, the only reason I write this post right now is
because I around 16.00 today forgot adding a file to my repository at work —
making it impossible for me to work this evening.
Oh well, I will just sit down with a cup of coffee and relax.
In the past we at Aalborg Soobak had a Taekwondo Quiz. The game is about translating words form korean to danish in rounds. In each round a word to translate was provided along with a list of possible translation. The player then had to select the correct translation. During the game, the player was awarded points – the game was over at the first wrong answer. To make it a bit more difficult, the answers had to be given within a given time frame.
The quiz, however, has not been available on our web-page for a long time. We have renewed our web-page and the quiz got lost in the modifications. The game has however been requested quite often by other clubs ( but strangely enough by our own membes ) and everytime we responded: “We are aware of it. It will come back eventually. ” – but we never implemented.
One day I received an e-mail asking if the quiz would re-emerge as they were missing it. As mentioned, we already intended to reimplement the quiz and it had just been pushed back in the pile of tasks for ages. Anyway, I had the day off and in classic programmer style thought: “I can do this in two hours – I will be done before lunch” (I started in the morning around ten). I was not finished before lunch – in fact I did not finish before 23.00 in the evening with a reimplementation using the old HTML-code.
I could have been done earlier, had I not spend time focusing creating a decent architecture for the PHP back-end. Something that paid as I two days later – with minimal effort – could change the front-end completely to use bootstrap and be a responsive web-page (comes for free with bootstrap).
I have some improvement planned for the taekwondo quiz, but they will have to wait. The quiz is available here ( only in danish though)
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”
I have a paper deadline just around the corner. I usually try not to plan any events in the weekends before paper deadlines as I know I will want to edit the paper in the weekends as well –I’m most efficient in the weekends and in the evenings. This time I however had planned to attend an event. A birthday party in Oslo. I have a paper deadline just around the corner and that and usually I try not to plan any events in the weekends before paper deadlines as I know I will want to edit the paper in the weekend as well –I’m most efficient in the weekends and in the evenings. This time I however had planned to attend an event. A birthday party in Oslo.
Continue reading “Travel Time”