Michael Jones, PhD

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.