© 1996-2006 Bell Laboratories
VeriSoft is a tool for Systematic Software Testing.
summary is available.
Customers. VeriSoft is a tool for software developers and testers
automatically searches for coordination
problems (deadlocks, etc.) and assertion violations in a software
system by generating, controlling, and observing the possible executions
and interactions of all its components. It integrates automatic
test generation, execution and evaluation in a single framework.
VeriSoft includes an interactive graphical simulator that can drive
existing debuggers for examining precisely the concurrent execution
of multiple processes.
Benefits. VeriSoft can quickly reveal behaviors that are
virtually impossible to detect using conventional testing techniques, and
hence reduces the cost of testing and debugging, while increasing
Scope. VeriSoft can test software applications developed in any
language (C, C++, Tcl, etc.). VeriSoft is optimized for analyzing multi-process
applications. It can analyze systems composed of processes described by
hundreds of thousands of lines of code. Source code for all the components
is not required.
Technology. The key technology used
in VeriSoft is a new form of systematic state-space exploration
(also called "model checking" in the research literature). With
its first prototype developed in 1996 and its design first presented
at POPL'97, VeriSoft is the first software model checker using
a run-time scheduler for systematically driving the executions of an
application through its state space.
Visit the VeriSoft Web-site: