Abstract Interpretation

(source ilachinski.com)

I realized I don’t write a lot about what I’m actually doing day in day out for work. This is partly because it is thought as “hard to describe” to non-computer science people. Today, I want to describe a method which is widely used in the software verification community in an easy way.

The technique is called Abstract Interpretation (AI from now on) and has been first described by Cousot in 1976/77 [1]. Now, to describe AI I’ll directly start with an example also partly taken from [1]:

Imagine you are presented with the following calculation .

Now I’m asking you to tell me the result of this multiplication without the help of a calculator. Obviously, unless you are a scary person, you don’t know the result because it is too complex to calculate in your head. However, when I change the question and ask you to tell me the sign of the result of this multiplication you will tell me instantly that the result is positive. How did you know that? Most probably you used your old highschool knowledge that the multiplication of positive numbers yields a positive result. So you used, without actually realising it, an abstraction of the multiplication operator to get the correct answer. This is a kind of abstract interpretation.

What we learned so far is: Abstract interpretation is replacing the actual domain of the answer (in our case the set of integers) with an abstract domain, in our case the sign domain which has only two elements . Also, it is replacing the normal operations with abstract operations. Our abstract multiplication operation has the following properties on the sign domain:

Now all that is missing is an abstraction function from the concrete domain to the abstract domain. This is defined as follows

Using these definitions we can easily solve the problem from above:

Now you could define more abstract operators on the sign domain and you would end up with a full abstract interpreter for basic mathematical operations. Cool, isn’t it?

To sum up, this technique is simplifying a problem by abstracting away information you don’t need to solve the problem (e.g. only getting the sign of a computation). The nice thing then is that the more abstract version is easier to calculate and the abstract result is saying something about the concrete result!

Of course, the sign domain is very primitive and has only limited use. Real abstract interpreter support many different abstract domains but the idea is always the same.

—-

[1] Cousot, P. and Cousot, R. 1977. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (Los Angeles, California, January 17 – 19, 1977). POPL ’77. ACM, New York, NY, 238-252. DOI= http://doi.acm.org/10.1145/512950.512973

http://www.di.ens.fr/~cousot/COUSOTpapers/POPL77.shtml

Boxing Day

Yeah, Merry Christmas and everything. So, in Switzerland we even got the privilege of a white Boxing Day. The 26 December is called Boxing Day in English speaking countries. Wikipedia reveals that this is because “to give a Christmas-box (colloq.); whence boxing-day.”.

Parallel Universes on Sunday Evening

 

About two months ago, a few popular science magazines and newspapers reported on a new discovery of a proof that parallel universes exist. Dr Deutsch, a mathematician from University of Oxford, seemingly found the proof for something which only existed in theories so far: parallel universes — infinitely many universes only a hair’s breadth apart from our reality, floating in the 11th dimension.

However, I had no idea if this is actually a true story or just a somewhat sensational report on a paper somebody didn’t understand. Since I don’t trust newspapers and since my knowledge of quantum mechanics is limited to wikipedia-depth I thought I’ll ask those who should know: Our physics department has its own Centre for Research in String Theory. Cool, isn’t it? So, I picked the head of this group and decided to write him a mail with my fundamental questions.

Now, after 1.5 months, I still haven’t received a reply 😦 .

Busaba Eathai

(picture urbanpath.com)

Last Saturday I went to Busaba Eathai in Soho (btw it is directly beside the Swiss restaurant St. Moritz and up the road of Hummus Bros!). Don’t let yourself put off by the long queues outside this popular restaurant. They let people in by the size of your group.. so if you go with two people you are almost certainly quicker than a group of six! Inside you share a large table with few other people however that should not bother you because everything is pretty stuffed anyway. The service is friendly and quick; the food itself is good (can’t really judge Thai food though..) to a very reasonable price for central London.

The toilets are surprisingly clean (remember to judge a restaurant by its toilets) but watch out, the cleverly designed, shared wash basin allows you to spy in the female toilet and the other way around (of course, I did not do that! 🙂 .. or did I?)!

All in all a very good restaurant with a nice atmosphere suitable for quick dinners. However, don’t go there if you want to spend a long, nice evening because they quickly and friendly push you out (“No we don’t kick you out it’s just that there is a large group waiting outside”) as soon as you’ve finished eating.

Home

Finally at home again. I sort of forgot how a real winter feels like! Wow it’s cold here…

As a warm welcome to my holiday (ok that was a joke, we never make holidays of course) I received 16 XSLT (an ugly programming language) programs to grade. However the lecturer didn’t say how to grade. So I don’t know if from 1 to 10, to 25 or A to F; not to speak about what criteria are needed to reach these marks. Just a “mark until mid-January” mail. Oh well … one thing is for sure, it’s good the students don’t know that I am the one who marks them. Because in my opinion too many people pass this MSc course.. hrhr 🙂

xmas break!

Tomorrow evening is my flight back to Switzerland. I hope my flight this year will be better than the one from last year!

Ich werde bis und mit erster Januar Woche in Basel bleiben..

Google Queries

Every once in a while, it’s funny to see how people find my blog here. The latest google searches leading to the blog are:

• “money”
• “big women” (wtf?!)
• “fat wommen” (whaat?!)
• “September 11 bank account” (wasn’t me)
• “kaputte zähne” (still a classic. No idea why)
• “was sind instant haferflocken” (good question..)
• “be different or die” (hmm..)
• “666” (oh oh)
• “lifttüren” (sorry to disappoint you)

Christmas Dinner #73992, Holiday

Today we had the Joint CS/EE (computer science, elec. engineering) Xmas (Christmas) dinner (actually lunch).
The figures speak for themselves. From Computer Science 6 PhD Students and about 4 lecturers turned up, from EE a whooping 70+ persons signed up for the lunch at a nearby restaurant. Apparently, the EE department organised the music and entertainment on their own. This meant we had to listen to self-taught Chinese (EE is mostly populated by Chinese people .. don’t know why) singers — this was cute but on the same time a bit miserable. At least it fit the food we had to eat (and digest now). Goat cheese cake with onions, then some Turkey (apparently, not sure if it really was meat) and then a slimy ball of Profiterole.

This started at 12pm. Later on we went back to our “informatics hub” and had another drinks+food party organised only by our department. This went on until now. I, in comparison to some work mates, am still capable of writing this entry 🙂 which is good.

In other news, I’m heading home on the coming Wednesday 19 December. That is good too! I will stay in Basel until 6 January. See you there hopefully!

Graduation

Gestern war meine Master graduation ceremony. Ich musste mich mit einer Gown bekleiden lassen (man wird von Helferinnen angezogen!) und danach mussten/durfen wir in der Great Hall die ueblichen Abschlussreden anhoeren. Das ganze war jedoch sehr formal und festlich. Eine ganze Belegschaft (hab den korrekten Namen vergessen..) von Dozenten von allen Departments waren auf der Bühne vertreten in verschieden farbigen Gowns, welche warscheinlich alle eine spezielle Bedeutung haben :).

Nach den Reden wurden alle Studenten einzeln auf die Bühne geholt und der QMUL principle conferred (übertrug) einem den MSc Titel symbolisch mit einem Händedruck. Danach musste man einwenig weiter gehen auf der Bühne und dem Head of Department nochmals die Hand schütteln. Darauf durfte man die Bühne verlassen.

Hier ein ziemlich miserables Foto (warscheinlich kommen später noch bessere) vom ersten Redner:

Nach der Feier und nach unzähligen Fotos vor der Uni gab es einen grosszügigen Apero mit viel frischen Brötchen und Champagner.

Der Zeremonie und Apero Marathon war jedoch noch nicht beendet. Es ging direkt weiter zum Department of Computer Science, wo in unserem “Informatics Hub” (quasi Aufenthaltsraum für Mitarbeiter) eine Department-eigene Preisverleihung stattfand.

Alles in allem eine sehr gelungene Abschlussfeier. Ich bin froh, diese in ein paar Jahren nochmals erleben zu dürfen. Dann jedoch in einer roten gown 😉 …

Rebtel

If you need to make frequent calls to international mobile phones you got to be prepared to pay a lot. Even if you’re using SkypeOut it’s just darn expensive. Another VoIP service called Jajah does not help either. A few days ago I found Rebtel which seems to do an excellent job. It’s half (!) the price of Skype to call international mobile phones and if you have free minutes, you can make mobile-to-mobile calls for free! Very empfehlenswert.