« July 2005 | Main | September 2005 »
August 29, 2005
[Misc.] Duck Creek Village utah
For a funky good time in Utah, go visit Duck Creek Village (the real one, in person). You'd think you were smack dab in the middle of a hippie commune in the 60s. It was fun and our twins had a great time throwing rocks into Duck Lake. Unfortunately, the village meadow was flooded so Duck Creek Days or whatever it was was cancelled.
Posted by jones at 10:05 PM | Comments (0)
August 23, 2005
[Research] Update from SPIN 2005
I am at SPIN 2005 in San Francisco this year. Its been an interesting conference so far. Here are a few things I am thinking about.
As processors go multi-core with shared memory, an interesting problem for model checker tool builders is: how do you exploit multi-core shared-memory machines? Its related to the parallel model checking problem, but involves a different architecture. (From a conversation with G. Holzmann).
Counter-example guided abstraction refinement (CEGAR) is cool and lots of people think it has a good future. There are some interesting questions yet to be answered. First, how to deal with more complex data operations and data structures? CEGAR tools use some form of automated reasoning to support the abstract interpretation of a program relative to a collection of predicates. The kinds of data operations supported by a CEGAR tool is limited by the kinds of data operations that can be reasoned about by the decision procedure support in the theorem prover. Two specific things have come up so far:
- Often, people use the low-order bits of a pointer to encode some data. This is particularly common in device driver and other hardware/software interface code. For example, one might use the bottom two bits of a pointer to enocde something about the status of a device. The question for CEGAR tools is how to recognize and reason about this data. (from conversation with B. Cook). I don't quite understand the problem, but that's the fuzzy picture I have so far.
- Work on arrays so that one can correctly reason about array indices. More to come on that one as papers get published.
Machine code is not a dead problem. People care about it. But, the big question for us as Estes writers is: how are you going to reason about machine code symbolically? The problem with Estes is that gdb isn't quite set up to reason about symbolic values. However, if we went to Bogor and we finished our symbolic bogor implementation, then we would have a platform for identifying and playing with the problems that will arise in symbolic model checking of machine code. The other and perhaps more interesting problem would be to think about how to do CEGAR on machien code using GDB.
Posted by jones at 12:51 PM | Comments (0)
August 18, 2005
[Misc.] this is a test.
Posted by jones at 11:26 AM | Comments (0)