checking the gc correctness

[Dan Nicolaescu]

Hi!

A research group at Stanford has developed a tool for formally
checking different properties of a program. 
The properties are described in a language that they developed, and
the descriptions are said to be realy small (~100 lines)
They use a modified version of gcc and their language to do this. 
(they hook into the parser and analyse the CFG)

They have used their system to find locking problems in the Linux
kernel (and many other things). 

You can find more details about this at: 

http://www.stanford.edu/~engler/


Their tools have not been released yet...  
But somebody (maybe Gerd) can ask them if they want to run their tool
on Emacs to check the gc correctness.

It's probably very easy to describe the gc rules: all lisp vars should be
protected before calling a function that can collect (mind that I'm no gc
expert), etc. 

Just my 2 cents...
        --dan