Skip navigation

Last week, a bunch of us from U. Iowa (8 in total, in two rental cars) drove down to Kansas U. for Midwest Verification Days (MVD), hosted by Perry Alexander and Andy Gill, and very efficiently supported by the wonderful staff there at the Kansas Information and Telecommunication Technology Center (ITTC).  As has become the norm for MVD, it was a lively meeting, with around 60 participants, and a very high level of talks.  Most of the talks were from graduate students, though undergraduate Angello Astorga (who worked with me this past summer) came down from Ohio State to talk about his summer work, and there were also great industry talks by Lee Pike of Galois and Ray Richards and David Hardin of Rockwell Collins.  You can see the full schedule on the MVD ’12 page.  Galois and Rockwell were both in recruiting mode, as well as telling us about the amazingly cool applications of formal methods that their companies are pursuing.  I would love to see MVD become a recruiting event, as well as a research event.  We are clearly on our way with the presence of these two important formal-methods teams.

As I said, the student talks were really great.  I personally always love hearing the talks from the U. Colorado Boulder group.  They are always doing some cutting-edge applications of static analysis or formal methods to current development problems.  For example, Arlen Cox and Devin Coughlin were talking about static analysis for Javascript — very relevant for web programming, of course, and posing nasty analysis problems as the language and idioms for it are very dynamic (e.g., method calls by reflection) and hard to deal with statically.  Sam Blackshear  was talking about live-leak detection, which I always thought was an intriguing problem.  Really, all the talks were great, and I don’t have time to tell you about all of them.  So I have to just mention a couple more.  I really liked a talk by Caleb Eggensperger of U. Oklahoma on ProofPad, a nice graphical interface for ACL2.  The talk by Dongjiang You of U. Minnesota Software Engineering Center on Observable MC/DC (a code coverage method I’d heard his advisor Mike Whalen talk about before), was also very interesting to me: the idea I took away (and I’m not too familiar with code-coverage techniques) was that we could execute a piece of code with concrete inputs, while still tracking which internal variables contribute to the output.  This could help us see which internal parts of a system are being exercised by a concrete test case.  That’s a cool mix of static and dynamic semantics (since we have a dynamic execution that tracks some static information, namely which variables contributed to a concrete value), which I had not considered before.

Anyway, it was a really fun event, and I’m very pleased that MVD is alive and well, following what is now the 4th edition (MVD ’09 and ’10 were the first ones, at Iowa; and then MVD ’11 was at Minnesota).  MVD ’13 will be at U. Illinois Chicago, hosted by Lenore Zuck, who was also there at MVD ’12, so that is going to be very exciting as well.  Our definition of the Midwest is pretty broad, and Midwesterners are welcoming people by nature: so swing by for the  next one if you can.


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 )

Twitter picture

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

Facebook photo

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

Google+ photo

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

Connecting to %s

%d bloggers like this: