MVD ’10 was a pretty big success this past Friday and Saturday, in my opinion. We had talks ranging from automated software testing to real-time systems to type theory. It was a bonanza of a verification and static analysis. I’ll mention just a couple talks that made an impression on me. It was a great program overall, so these are really just a selection from many very good presentations.
Pingyu Zhang presented work with his advisors at U. Nebraska on using symbolic simulation to generate stress-tests for software. The goal of their work is to find programs input that lead to long executions. Pingyu gave the example of asking an App using Google Maps for an optimal route connecting a bunch of locations: essentially the NP-hard traveling salesman problem. While most inputs to this App manage to get solved heuristically in reasonable time, their technique is able to generate inputs that cause it to take 1 day to complete! Wow. Pingyu’s presentation was quite clear, although I didn’t comprehend the details well enough here to explain their method. What is sticking with me most is the problem itself: find inputs that lead to long execution times. This is quite interesting, and quite a bit different from the usual verification problems of searching for violations of invariants.
To highlight just one more talk, I cannot help but praise Jan Vitek for a really riveting invited talk on “Is Java Ready for Real-Time?” This was an amazing tale of how a language that really has no business being considered for real-time applications can actually be tamed for that domain. Jan touched on really impressive work on real-time JVMs, including a quick tutorial on real-time garbage collection, a topic I have been wanting to learn more about. He presented some work from a PLDI 2010 paper of his titled “Schism: Fragmentation-Tolerant Real-Time Garbage Collection”. This combined several interesting ideas from the literature to get what sounds like the world’s best real-time GC: completely reliable, close to the performance of a non-real-time GC, and low fragmentation (which afflicted other recent approaches, apparently). This is really cool work, which I am itching find some time to read more about.
As I said, there were many more very good talks (the students from the CU Boulder PL group had some pretty original ideas on software analysis, for example; and there are many more). We are still working to line up MVD ’11, but hopefully that will happen (somewhere other than Iowa City, because two years in a row is enough). So keep an eye out for that, if you are in the Midwest, reasonably broadly construed.