Model Checking for Fun and Profit

So, I'm starting to fall in love with model checking. It looks like it will lead to much of what I'm looking for from formal verification: user friendliness, push-buttonness, and utility in actual software development amongst other things. Now, it's never going to enable you to do full functional correctness on anything but the most trivial of programs, but that's not what's needed most of the time. Simply bring model checking to bear in a big way in normal software development would be a huge step forward for both formal methods and software engineering. Projects like SLAM are wonderful examples of the utility that a properly designed and integrated formal methods suite can bring to bear.

Billie G and the Boys

Turns out the Eclipse problem wasn't versioning, but rather syncing. For some reason, I had told unison not to sync ".metadata" directories. Naturally, this kept the Eclipse project metadata from getting copied over, yadda yadda yadda.

Anyways, Bill Gates gave a lecture today at UT, talking about the future of software etc. Most of it was standard "exciting time to be in CS" boiler plate that he's clearly given a million times, but some things he said were actually interesting. In particular, he made a brief statement about higher level languages, and how he doesn't believe that we are operating at a high enough level yet. In particular, he claims that we can get to within an order of magnitude of density of English specification. It made me realize that I'm not very familiar with the recent developments in highly dense and readable programming languages. I'm vaguely aware of Joy and Icon, but I don't have enough experience to speak on them.

P.S. If you can't tell, I'm turning this more into an actual blog/work journal. I started looking around for an application to do journaling when I remembered that I had this already set up!

Little bit of thinking, not much working

Today wasn't very productive. I got up early, waited in line (along with ~70 other idiots) to get my bracelet for the Bill Gates talk on Wednesday. Later that day I discovered that there was quite a surplus. Oh well.

I raced home and ran up to work. Once there, I did a whole lot of nothing for 2 hours. On the plus side, I figured out how to auto-forward my Lotus Notes mail to my outside address (use filters!), so I shouldn't need to actually go into NI as often. It'd be even easier if I had figured out how to setup Lotus on my laptop for remote access, but oh well. I don't want no stinking Lotus code on my nice clean laptop anyways.

I ran back home and then biked back to UT in time for the PL Lunch. While enjoying my tasty BBQ, I heard an interesting presentation on "Repairing Data Structures using Assertions" by Baseem Elkarablieh (dry run for his thesis proposal). In a nutshell, he used a boolean function (repOK()) that verified the integrity of a data structure to generate a search for a new data structure that satisfied the repOK() predicate. The basic approach is little more than an application of constraint solving (hardly novel when you consider their uses in test generation), but the really cool stuff came out of his work using static analysis to optimize the search process. On (moderately) complicated structures, he saw an order of magnitude increase in performance.

Relevant papers:
Assertion-based Repair of Complex Data Structures
STARC: Static Analysis for Efficient Repair of Complex Data

Afterwards, I ran home yet again (I'm going to be sore tomorrow) and tried to get cracking on some ideas I've been researching for work. But, I kept coming up with excuses for why I couldn't start working just yet; "My computers are out of sync" (run unison), "My folders are disorganized" (move massive files to file server, delete crap), and finally, the biggie: "Eclipse doesn't work". This is the only remotely legitimate excuse I came up with. See, for some bizarre reason, even though I synced my Projects directory between minerva and mercury, my work project workspace didn't show up in mercury. I suspect that this has to do with some subtle version difference between the Eclipse versions in Feisty and Gutsy (minerva is Gutsy), so I'm finally getting around to upgrading my long lived and trustworthy install of Feisty. It'll take a few more hours, so we'll see how it went in the morning...