KeY

Deductive verification and symbolic debugging for Java. Specify behavior in JML; KeY proves correctness or finds bugs. Symbolic Execution Debugger integrates with Eclipse. Used in teaching and research.