NASA Logo, National Aeronautics and Space Administration

Symbolic Execution

The objective of the automated testing project is to perform automated generation of test inputs that obtain high coverage for flexible (user-definable) coverage metrics and to check properties of code during test case generation.

To this end, we have developed a tool, Symbolic JPF, that combines symbolic execution with model checking and constraint solving for test case generation. In this tool, programs are executed on symbolic inputs representing multiple concrete inputs. Values of variables are represented as numeric constraints, generated from analysis of the code structure. These constraints are then solved to generate test inputs guaranteed to reach that part of code. Essentially Symbolic JPF performs symbolic execution for Java programs at the bytecode level. Symbolic JPF uses the analysis engine of the Ames JPF model checking tool.

Symbolic JPF

  • Performs symbolic execution of Java bytecodes
  • Handles complex math constraints, data structures and arrays, multi-threading, pre-conditions (on-going work)
  • Applies to (executable) models and code
  • Generates test vectors and test sequences that are guaranteed to achieve user-specified coverage (e.g. path, statement, branch, MC/DC coverage)
  • Measures coverage.
  • Generates JUnit tests, Antares simulation scripts, etc. (output can be easily customizable)
  • During test generation process, checks for errors
  • Is flexible, as it allows for easy encoding of different coverage criteria
  • Is integrated with simulation environment (on-going work)


Test input generation for Java container classes, NASA guidance navigation and control (GNC) software; script generation for testing execution engines.

Other info

Combining Unit-level Symbolic Execution and System-level Concrete Execution for Testing NASA Software (paper published in ISSTA 2008 proceedings)

Symbolic JPF -- Symbolic Execution of Java Bytecode (presentation given at JPF workshop, MSR, ISSTA 2008)

Symbolic JPF is freely available from (extensions/symbc). Tool documentation (old).

Updated 2017

Project Members

Corina Pasareanu
Peter Mehlitz

Past Members

Willem Visser
Karen Gundy-Burlet
Hamed Jafari
David Bushnell

Summer Interns

Mithun Acharya
Suzette Person
Saswat Anand
Radek Pelanek
Sarfraz Khurshid

Related Projects

JFuzz from MIT

First Gov logo
NASA Logo -