Separation Logic

Now it’s official that the topic of my master thesis will be related to Separation Logic. My supervisor is Jan Schwinghammer from the Programming Systems Lab of the Saarland University.

Last night I couldn’t fall asleep until I wrote an email to Jan to tell him about my decision. Telling him was very important because I don’t want to be tempted to try escape when I will see how hard these things really are. Now I hardly understand anything about them, but the topic looks promising and very challenging at the same time, and this is more than enough to motivate me to try my best.

Separation Logic is a sub-structural logic that supports local reasoning for imperative programs. It is designed to elegantly describe sharing and aliasing properties of heap structures, thus facilitating the verification of programs with pointers.


One Response to Separation Logic

  1. I told my mother that this was the hardest problem I was able to find so that is why I’ll do it. Then I thought a little about it … there was also P = NP but nobody asked me about it 😉

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Google+ photo

You are commenting using your Google+ account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )


Connecting to %s

%d bloggers like this: