POPL + PLMW Update

Posted on by Heidy

Truly, I am guilty of abandoning this blog. I graduated in December 2012, and that was quite stressful. A few people approached me and mentioned that I should update my blog! Fortunately, after attending POPL 2013, I was quite inspired to start blogging again. I will update my blog every other Sunday, at the very least, as that is the only day where I do have a bit of free time. Where am I now? I’m back at Microsoft Research Cambridge, working again under Byron Cook. This post will have two parts, the first being what I am doing now at MSRC, and the second being an update pertaining to POPL 2013 in Rome.

Temporal Property Verification at MSRC

In Summer 2012, I began implementing Cook’s Temporal Property Verification as a Program Analysis Task in T2, Microsoft Research’s predecessor to Terminator. This went quite well! Towards the end of my first internship, Abigail See improved the termination aspect of our tool through Lexicographic Ranking Functions.

The tool took quite some time to implement, but towards the end of my internship we started brainstorming  various ideas to improve the scalability of our tool. Hence why I’m back at MSRC! We’re currently discovering scalable methods for checking temporal properties. We plan to design better techniques that can be crafted by adapting methods drawn from abduction, interpolation, and precondition synthesis. Byron and I are now working on Bottom-Up Temporal Property Verification of Infinite-State Transition Systems. If our plan goes as desired, I will most likely write a more detailed post pertaining to this project.

POPL + PLMW 2013

This year I received the PLMW Scholarship for the second time. PLMW was hosted last year in Philadelphia, and it was quite an honor to attend the very first instance of it. The second annual PLMW was hosted in Rome this year (alongside POPL13), and I’m grateful to be able to attend it twice. I must say, I was quite impressed with how they acted upon the recommendations we had for the PLMW organizers. They recruited significantly more undergraduates than last year and they put  together a variety of excellent and insightful talks. To my surprise, my experience at POPL13 was vastly different from last year’s.

As mentioned in my previous blog post, I decided to switch my research focus from Type Theory to Model Checking and Verification. Given how I was an absolute novice to Verification, I barely understood any of the talks that I attended last year. However this year, I attended all the talks specific to my area, and I was impressed with how well I was able to understand the vast majority of them! I suppose after 8 months of involvement, you learn quite a bit. This vastly altered my experience in comparison to last year’s, as this year was much more of a learning experience than a discovery/networking experience. Without further ado, here were my favorite talks at POPL13 (In chronological order):

Inductive data flow graphs.
A. Farzan, Z. Kincaid, A. Podelski

Abstract conflict driven learning.
V. D’Silva, L. Haller, D. Kroening

Views: compositional reasoning for concurrent programs.
T. Dinsdale-Young, L. Birkedal, P. Gardner, M. Parkinson, H. Yang

High-level separation Logic for low-level code.
J. Jensen, N. Benton, A. Kennedy

The ramifications of sharing in data structures.
A. Hobor, J. Villard

A few of these talks are what inspired my new found interest in Abstract Interpretation. Zach Kincaid is currently interning with Byron as well, and he has been a great personal motivator towards learning Abstract Interpretation (It’s his expertise!). I have also been interested in Separation Logic since having a few conversations with Peter O’Hearn last year. I’m mainly interested with how it ties into verification of concurrent programs (A common theme at this year’s POPL). Not enough time exists within the next year for me to fulfill my research aspirations!

Overall, I will not be attending PLMW again, as I felt that I was much more aware than the vast majority of the students attending. I have concluded that I will only be attending POPL again when I have successfully submitted a paper. Hard work here I come!


Leave a Reply

Your email address will not be published. Required fields are marked *