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.