Readme

Symbolic (Java) PathFinder:
---------------------------

Created new branch that contains many updates to SPF;
in particular, interfacing with Z3 is robust; 
also SPF now has a "symcrete" mode that executes paths 
triggered by concrete inputs and collects constraints along the paths

This JPF extension provides symbolic execution for Java bytecode.
It performs a non-standard interpretation of byte-codes.
Currently, it allows symbolic execution on methods with arguments of basic types
(int, long, double, boolean, etc.). Symbolic input globals and method
pre-conditions are specified via user annotations (see symbc/examples and
symbc/test).

A paper describing Symbolic PathFinder appeared at ISSTA'08:

Title: Combining Unit-level Symbolic Execution and System-level Concrete
Execution for Testing NASA Software,
Authors: C. S. Pasareanu, P. C. Mehlitz, D. H. Bushnell, K. Gundy-Burlet,
M. Lowry, S. Person, M. Pape.

Tool documentation can be found at:
http://babelfish.arc.nasa.gov/trac/jpf/wiki/projects/jpf-symbc