Monday, June 11, 2012

Greetings from Beijing!

Hi Folks,

My name is Ming, and I'm an nth year PhD student at UC San Diego (consider your favorite, or least favorite n...). Although I believe we students were asked to contribute to this blog prior to the conference starting, I'm afraid I'm a bit tardy and instead am posting while enjoying the first day's sessions.

In theory, I am here to present my paper on statically proving the determinism of parallel programs using the Liquid Effects system. In fact, I have already given the presentation and will instead be enjoying the rest of the conference program.

I believe there are at least a few concrete benefits I am getting out of attending this PLDI, but I will limit myself to discussing two of them.

1) Every conference I attend, I find myself exposed to at least 2 or 3 new problems that I had not previously considered, but due to either the persuasiveness of a presentation, or a conversation with another attendee, thereafter decide to be paramount to scientific advancement.

2) From speaking to other researchers, I often get the feeling that our work on refinement types is considered by some to not be generally accessible. However, my feeling is that the truth is exactly the opposite -- and that our goal is and has been to make both the inputs and outputs to verification maximally accessible to both practitioners and other researchers.

However, it can be hard to get this across in the technical paper; the conference talk, on the other hand, is a much better arena for this, because it can emphasize the action of the tools that result from our work. Hopefully, the talk I have constructed serves this purpose, and I have done my colleagues a favor in spreading understanding of their hard work to those who might have dismissed it immediately if only exposed to the paper.

Finally, I'd like to end with some shameless self-advertisement. For more information about our paper, and the associated Liquid Types project, please visit the following URLs:

http://goto.ucsd.edu/~rjhala/papers/deterministic_parallelism_via_liquid_effects.html
http://goto.ucsd.edu/~rjhala/liquid/

Further, releases of our tool CSolve, for proving assertion safety and determinism of C programs, can be found here:

http://goto.ucsd.edu/csolve/

Thanks for reading, and I hope everyone enjoys the rest of the conference!

--Ming

No comments:

Post a Comment