IDebug is an advanced debugging framework for Java. It provides the standard core debugging and specification constructs such as assertions, debug levels and categories, stack traces, and specialized exceptions. Debugging functionality can be fine-tuned to a per-thread and/or a per-class basis, debugging contexts can be stored and recovered from persistent store, and several aspects of the debugging run-time are configurable at the meta-level.
JavaFE is a Java front-end that parses Java 1.4 source code and Java 1.5 bytecode. It is used as a compiler front-end for several research tools, including ESC/Java2 and RCC. JavaFE has a partial formal specification and, because it is a hand-written lexer, parser, and type checker, is very efficient.
KindFTP is meant to be a complete implementation of the FTP protocol, as specified in RFC959. It provides a component that directly exposes the low-level protocol, and it supports the core protocol that is available on most Open Source FTP servers. It has untested support for ACCT, SMNT, REIN, TYPE, STRU, MODE, ALLO, and SITE command. It uses iContract to provide a full formal specification of all software, jUnit for all unit testing, and Ant as a build tool.
The Mobius verification environment supports the development of specifications, programs, and proofs of their security properties. It will support both source code and bytecode level verification, and be able to produce the output necessary for the generation of PCC certificates.
OBJ3 is a program specification and proof system based on order sorted equational logic. It has been successfully used for research and teaching in software design and specification, rapid prototyping, theorem proving, user interface design, and hardware verification, among other things. It was the first language to implement parameterized programming and its module system influenced the designs of the Ada, C++, and ML module systems.
Votail is an implementation of Ireland's method of Proportional Representation by Single Transferable Vote (PRSTV). The functional requirements derived from Irish electoral law are specified using Business Object Notation (BON) and the Java Modeling Language (JML). Formal methods have been used to verify the correctness of the software.