Subject: tool cbmc

From: "Tzahi Fadida" <[email-masked]>
Date: Tue, 21 Sep 2004 22:31:14 +0200

Did anyone try this ANSI-C debugging tool?
http://www-2.cs.cmu.edu/~modelcheck/cbmc/

I watched a seminar today with daniel kroening 
and this debugging tool is very very impressive.
It find bugs you could never have found with regular
debuggers. it utilizes SAT solvers and pretty cutting edge
science to find the bugs. the highlight is employing 
a method of unwinding loops to a degree in order to find
bugs. it is supposed, if I understand correctly, to virtually
run the program (not really run but as though it was running) and
find the problematic inputs.
Of course the overall problem is Hard of course, but 90% of the 
usual problems can be found and sadly, as I understand its only
for programs for embedded systems or short codes.
For example, the breaks system in trains.
I also watched it give you the more or less exact spot where
the bug originated from. in order to do it, it takes the 
tree of bugs and finds the root where the least of steps
caused the bug, or something of kind.

cbmc - http://www-2.cs.cmu.edu/~modelcheck/cbmc/

p.s. its supposed to be free to use, at least from
 the creator mouth daniel.

Regards,
	tzahi.

WARNING TO SPAMMERS:  see at
http://members.lycos.co.uk/my2nis/spamwarning.html