Michael Jones, PhD

« Mac OS X 10.4 Tiger Install and First Impressions | Main | CSS Reference »

May 09, 2005

Thesis topic ideas

These are some thesis topic ideas I chanced upon while working on a proposal.

• Hash compaction for learning Davis-Putnam SAT solvers. The solvers are limited by memory available to store clauses. Well, why doesn't one compute a hash signature for a clause, flip a bit at that location and move on? It works quite well in explicit modle checking. Of course, there is a chance that you will think two different clauses have the same bit flipped, which is no good. And there's the problem of reconstructing a clause rather than just checking its existence. So this one may not work out, but its worth spending a day or two to see if you could do something reasonable and what the trade-offs would be. If it looks promising, it might make a good topic.
  
• A parallel explicit state enumeration algorithm that also uses magnetic disk. Our homebrew algorithm for model checkign with magnetic disk is based on the traditional partitioned hash table algorithm for parallel mdoel checking. In our experiments, we got a 10% slowdown when using 1/3 RAM and 2/3 disk compared to the 3/3 RAM algorithm. So you'd think you could combine the two algorithms to make more efficient use of each node in the parallel algorithm by using disk on each node in the parallel algorihtm. Idealy, you'd get 3x the capacity for a 10% performance hit.
  
• This one is a little deeper and might be a good start for a PhD topic. It involves the abstraction of infinite state parameterized protocols in a way that is suitable for use in explicit state enumeration. There are two main problems with the abstraction in my dissertation. The first is that it does not allow universal quantification in the guards or actions of commands. The second is that it does not allow loops in the network. The research would be to add both. Since both are essential for modern IO protocols and shared memroy protocols. I think you could get universal quantification by doing a symbolic state representation based. I think you could get loops in the network using "feedback diamters" which describe the length of the shortest loop needed to observe all of the feedback behavior in a network that allows loops.
  

Posted by jones at May 9, 2005 11:13 AM

Comments

Posted by: jdneal at June 16, 2005 03:53 AM

Post a comment