MIT students Adam Kiezun and David Harvison developed a “concolic execution” extension and contributed to the Ames Java Pathfinder (JPF) distribution under the open source NASA license. Concolic execution allows mixed concrete-symbolic execution of software, to enable efficient automated test case-generation that achieves high code coverage, without any user interaction. The new extension is based on Symbolic JPF, the symbolic execution mode in JPF, and effectively complements the test case generation work that is done at NASA Ames. This is another proof of the traction that JPF, and in particular Symbolic JPF, has gained in the research community.
NASA PROGRAM FUNDING: Symbolic JPF is funded under EDTP ISD.
Contact: Corina Pasareanu