GitHub - grzesuav/jpf-symbc: Mirror of http://babelfish.arc.nasa.gov/hg/jpf/jpf-symbc on github

Branches Tags

Name		Name	Last commit message	Last commit date
Latest commit History 608 Commits
.externalToolBuilders		.externalToolBuilders
bin		bin
doc		doc
eclipse		eclipse
launch		launch
lib		lib
nbproject		nbproject
prettyprint		prettyprint
src		src
tools		tools
.classpath		.classpath
.hgignore		.hgignore
.project		.project
Readme		Readme
ReadmeMultipleDecisionProcedures		ReadmeMultipleDecisionProcedures
build.xml		build.xml
dreal.readme		dreal.readme
jpf.properties		jpf.properties

Repository files navigation

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

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