TPHOLs + Munich
I’ve split this blog post into a section about the conference, and another about Munich so people can read whatever is appropriate to their interests. Its a big one guys.
I’ve just got back from TPHOLs, and I really enjoyed it. I only submitted an ‘Emerging Trends’ Paper, which doesn’t really count for anything, but the feedback from talking to people seemed worth while and positive. I even talked to a guy who had the rest of a compiler verified, using the same semantics as I do, and really wanted my work done so there was an optimising phase. Sounds like an excellent idea to me! Probably better focus less on this crazy bug fixing idea after all, and get back to some proper verification.
There were some really interesting papers, Quite a bit of low level code verification and techniques that viably work in ‘real world’ situations. Top of the list were the L4.Verified guys who were presenting two papers – one on extending their framework to include a separation logic for C and the other on their actual C Verification framework. I was surprised when talking to Gerwin Klein how few restrictions there were in their C subset. Allegedly they even have function pointers now – though it sounds like only verifying simple properties about them is sane at the moment.
One of the annoying feature about C is the non-determinism within the reduction of their expression semantics. Notably that evaluating an expression with a binary operator doesn’t have to evaluate its left hand side or right hand side totally first. Norrish’s original semantics for C capture this by bagging up side effects and then unbagging them non-deterministically – their new framework captures this, but for practical verification, they discharge appropriate proof obligations for common syntactic forms – eg expressions without side effects, functions calls with no reduction required in the arguments. This sounds like a fairly simple and reliable approach.
The Verisoft guys had some fairly heavy duty C verification tasks that they were undertaking as well – its good to see people attempting these large projects. They seemed to believe that they could finish in a year – quite impressive in my opinion.
The other thing I was surprised at was people making an effort at verifying properties of continuous maths, as well as traditional Computer Science. It somehow seems obvious with hindsight to define real numbers as a co-inductive definition, and operate on them co-recursively but I would probably have never made that intuitional leap myself – probably a side effect of not really reading any papers in that area. I always wonder how hard it would be to prove implementations of floating point arithmetic correct against a real number spec correct – I’m tempted to see if anyone has considered this kind of thing before, seems highly ambitious.
The conference organisers really deserve some credit for their efficiency – the directions were excellent, the hotel well chosen, things generally ran according to plan. We went on an excursion to a lake, which I had the utmost belief would result in people getting lost, but I don’t think anyone was at all. This was a complete masterpiece that totally validates my stereotypical belief in german efficiency. At certain key points, eg when a train would turn up or when we had to turn a corner – Stephan would clap his hands, and then all the local organisers would clap, and people knew what to do. The lake was picturesque, the Buccheim Museum interesting and the banquet excellent. Though I still haven’t figured out whether Zander is the German name for a fish I’ve eaten before, or a new fish.
I managd to forget to bring my camera, so any pictures I recall to put in will be efficiently cribbed from the internets. I visited the Englishgarten, which is a park near central Munich, containing a some splendid nature and a few interesting buildings.
I also had a wander through central Munich, which contains a few old buildings of varying architectural interest.
I had decided not to visit the workshops on the Friday of the conference, since I have less interest in Coq and none in Computer Algebra. I consequently spent the day acting as a tourist. I walked slowly, accidentally bumped into people, mumbled under my breath about the length of time it took for the road crossing lights to change and I even saw some of Munich! In the morning I went to the Deutsche Museum – which is a technology and engineering museum with a bit of SCIENCE thrown in for shits and giggles. This is what we should have more of in the UK.
We used to take family trips to Techniquest as a child, which was ok since it provided ways to play around with a cool demonstration of basic scientific principles, but I found it somewhat simplistic even at my young age, and I can’t imagine particularly enjoying it today. This place on the other hand went into low level detail about all sorts of engineering stuff – and had cool things for kids to play around with! Things like water wheels, boat sails, planes, damns, bridges, railways. This is really cool, and even gave me an idea for a simple physics game where you build a bridge. I’m sure its been done before – but might be cool to write anyhow maybe I can finally get round to learning some proper physics.
In the afternoon I went through the Residenz Museum, which is based in the Palace where Bavarian Royalty used to live, The Residenz. Unfortunately we bombed it to hell during the war, and its still being slowly restored. For example the facade is painted on plaster in some places, rather than being the original ornate part. Fortunately some of the interiors, and most of the fine art and furniture survived by being moved into the country. Really nice in some places, and it tells a bit about the way the Bavarian Dukes lived back in the day.
Afterwards I visited the hofgarden, beside the Residenz, walked around for a while, then sat down in the sun to have a beer. At this point in time it decided to rain … awesome. I managed to migrate myself so I was protected by a parasol and then ate a rather awesome slice of cheesecake. It was larger than my face. Then I wandered back to hotel via another park. Managed to get off at the wrong station on the train to the airport, its platform was marked with the word ‘flughafen’ which is German for airport, and I noticed this – it seemed a bit weird but I rushed to get off. I then realised that the sigh was saying “Flughafen Glies” – which meant it was the platform for going to the airport, rather than Munich city. Thankfully I had plenty of time, and trains were every 20 minutes. Plane flight back was ok.