NewsLetter 36 - January 29, 2003:Two new software distributions that relate to Spin vesion 4 have now been released by Bell Labs and are available from the web. Both packages include source code and documentation.
Uno is a simple, property based, static analyzer for ANSI-C code. It is available via URL:
Modex distributionModex is the model extraction program used by FeaVer. FeaVer was originally the name for the dedicated system that we built between 1998 and 2000 for the verification of the call-processing source code in one of Lucent's new switching systems. We later rewrote it to handle general applications in ANSI-C. FeaVer is now the name of the user-interface (there's a slick Tcl/Tk GUI and also a much simpler command-line interface) that uses the model extraction tool Modex to generate Spin Version 4 models for verification. The model extraction process is guided by a user-defined test-harness. All is explained in the user-documentation Doc/feaver.pdf that is included in the distribution. It is now available under Lucent's general non-exclusive source code license via URL:
End of Newsletter Nr. 36.