Software
ExMAn and ConMAn
Jeremy Bradbury, Jim Cordy, Juergen Dingel
ExMAn is an experimental mutation analysis framework supporting
the comparative evaluation of different fault detection techniques
such as model checking and testing using program mutation.
The ExMAn is now hosted
here.
ConMAn is a set of 24 concurrency mutation operators
for Java (J2SE 5.0). More information can be found
here
Embee and StateDumper Software
Juergen Dingel, Michelle Crane
Embee is a prototype runtime conformance checker
for Java programs. Embee takes as input an Alloy
specification (using a limited subset of the Alloy language)
and a textual configuration file provided by the user. It creates
several intermediate text files containing runtime information
which are used to check the conformance a specific breakpoints.
StateDumper is a separate, stand-alone program used by Embee
that retrieves the runtime information from executing Java programs.
It relies on classes and methods from the Java
Platform Debugger Architecture (JPDA) from Sun Microsystems.
Verisoft
Automatic Interface (VAI) Framework
Juergen Dingel, Hongzhi Liang
VeriSoft is a software model checker developed at Bell Labs.
It takes as input C/C++ programs in which concurrent processes
communicate through either semaphores, channels, or shared memory.
The VAI Framework works with Verisoft by providing the following
wrapper tools:
- VAI Front-End: Automatically transforms C/C++ IPC
objects to VeriSoft IPC objects.
- VAI Back-End: Provides a Java interface for paring
a VeriSoft trace file and accessing its content
