My project for the summer is to build a tutorial for FLAVERS, FLow Analysis VERification of Software, a static verification system for proving properties of software systems. That all seems pretty easy - first add some code, then some properties, a few constraints, hit "analyze" and go. But it's unfortunately that simple, since doing all that requires a thorough understanding of Quantified Regular Expressions and Finite-State Automata, concurrency, stuff like that. Which means that to write about it so that other people can understand it, I have to understand it first. A bit of a daunting task, but it's been fun.

Here's a link to my tutorial. I'll throw up updates every few days.

And so a kind of journal of my work:
5/23/01: Well, so far I've been swimming (and treading water, and screaming for help, alternately) in an acronym soup. I luckily haven't found any dead flies yet. I'm a part of the Analysis (as opposed to the Process) end of operations here at the LASER lab at UMass. The plan is that I learn to use a software system called FLAVERS and then write a tutorial to help other hapless outsiders like me learn to use it in an easier fashion. (Has anyone else noticed that people who formulate CompSci acronyms can't spell, or is that only something that gets to English majors?) This probably doesn't qualify as a "research project" as most people define one (I mean, the paper to turn out at the end is an expository set of instructions), but I'm certainly learning quickly, and hopefully my work will make a difference somewhere along the line.

6/01/01: I think I've managed to kind of figure out regular expressions (so far, the cord from my head phones getting in my way has been the least of my problems). I started drafting the tutorial (setting up the HTML file structure, working my way through the existing tutorial and updating it, etc). I spent a full day figuring out how to formulate properties of programs in Regular Expressions and Finite State Automata and all that, but I don't see the rest of the system being as difficult to get under my thumb. Things are certainly better already than last Friday, when people were tossing around technical terminology so fast that I thought I'd never catch up. Now I'm pretty sure that if I trained to be a marathon runner for two years, I could hold my own most of the time.

6/12/01: Spent the last week in the Cayman Islands with my parents! It rocked. I got to hold and feed a 150lb Southern sting ray. Other than that, lots of snorkeling, scuba diving, sailing, swimming, and sunning. Got some much-needed R&R. Should be pictures from the Caymans up at the Underground as soon as I get back to my scanner in August.

6/20/01: More work on QREs. Turns out, they're way harder than I expected. Go figure. There's a lot of syntax I don't understand. I'm also in the process of reading a lot of papers about static verification and analysis. Most of the math goes right over my head, but it's interesting stuff.

7/5/01: Spent a few days at home (Raleigh, in the Duke University area) visiting Mark (see the Underground for pictures). We had an awesome weekend. Saw some fourth of July fireworks here.

7/23/01: Woops! I completely forgot about this web page. Things have gotten a lot easier lately. I've mastered a lot of the acronyms and even begun to understand a lot of the material I'm writing about. It turns out that QREs aren't as hard as I thought because it's easy to make them needlessly complicated, and a bunch of the examples I was studying were. I've got properties of systems pretty much covered, including FSAs and QREs. I wrote a BNF for the first time the other day, and linked that up. There's a lot of cleaning to do now of the whole tutorial, but at the same time I'm getting started on constraints (which eliminate infeasible paths from the analysis and are also formulated as FSAs) at the same time.

8/16/01: Well, tomorrow is my last day on the job. The tutorial is reasonably complete, and I have a pretty decent handle on the world of finite-state verification of systems. Hopefully, the documentation I've done this summer will make learning FLAVERS easier on other people.

8/17/01: Outta here!