Java PathFinder (JPF)
is an Open-Source system contributed by NASA to verify
executable Java bytecode programs.
JDJ has an interesting
article on it, "NASA Open-Sources Java Pathfinder." This is a somewhat historic moment, as this is the first
Open-Source NASA program to be actively developed and hosted
on
SourceForge.