[Main]
[Tutorial]
[Demo]
[FAQ]
[Documentation]
[Download]
[Contact us!]
[About VeriSoft]
© 1996-2006 Bell Laboratories, Lucent Technologies
VeriSoft is a tool for Systematic Software Testing.
-
Customers. VeriSoft is a tool for software developers and testers
of
concurrent/reactive/real-time systems.
-
Description. VeriSoft
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
reliability.
-
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.
A one-page
summary is available.
Visit the VeriSoft Web-site:
