jonny goes to england

London & co

Archive for December 2007

Abstract Interpretation

with 2 comments

abstract-new-15.jpg

(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 3948 * 729 * 98573.

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 \{pos,\ neg\}. Also, it is replacing the normal operations with abstract operations. Our abstract multiplication operation \otimes has the following properties on the sign domain:

pos \otimes pos = pos

pos \otimes neg = neg, neg \otimes pos = neg

neg \otimes neg = pos

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

\alpha(n) = pos, \text{if } n \in \mathbb Z^{+} \cup \{0\}

\alpha(n) = neg, \text{if } n \in \mathbb Z^{-}

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

\alpha(3948) \otimes (\alpha(729) \otimes \alpha(98573)) = pos \otimes (pos \otimes pos) = pos

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

Written by jk

December 30, 2007 at 2:15 pm

Posted in english, technical

Boxing Day

with 2 comments

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.”.

Written by jk

December 26, 2007 at 9:19 pm

Posted in english, Switzerland, UK

Parallel Universes on Sunday Evening

with 2 comments

 paralleluniverses.jpg

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 😦 .

Written by jk

December 23, 2007 at 9:31 pm

Posted in english, QMUL

Busaba Eathai

leave a comment »

busaba-eathai.jpg

(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.

Written by jk

December 21, 2007 at 12:34 pm

Posted in english, food, London

Home

with 2 comments

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 🙂

Written by jk

December 20, 2007 at 5:25 pm

Posted in Basel, english, Switzerland

xmas break!

leave a comment »

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..

Written by jk

December 18, 2007 at 11:46 am

Google Queries

with 2 comments

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)

Written by jk

December 16, 2007 at 6:04 pm

Posted in english