-
Notifications
You must be signed in to change notification settings - Fork 91
Home
Symbolic PathFinder (SPF) 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 SPF performs symbolic execution for Java programs at the bytecode level. Symbolic PathFinder uses the analysis engine of the Ames JPF model checking tool (i.e. jpf-core).
Symbolic PathFinder
-
Performs symbolic execution of Java bytecodes
-
Handles complex math constraints, data structures and arrays, multi-threading, pre-conditions, strings (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. Symbolic PathFinder has been used at Fujitsu Labs for testing Web applications - see [http://www.fujitsu.com/global/news/pr/archives/month/2010/20100112-02.html Fujitsu press announcement]. See also [http://spinoff.nasa.gov/Spinoff2010/ct_3.html NASA’s post].
-
[https://github.com/SymbolicPathFinder/jpf-symbc/wiki/Documentation Documentation] for Symbolic PathFinder
-
[http://ti.arc.nasa.gov/m/profile/pcorina/papers/fp047-pasareanu.pdf Combining Unit-level Symbolic Execution and System-level Concrete Execution for Testing NASA Software] (paper published in ISSTA 2008 proceedings) — describes Symbolic PathFinder
-
[http://ti.arc.nasa.gov/m/profile/pcorina/papers/paper149.ps Generalized Symbolic Execution for Model Checking and Testing,] (paper published in TACAS 2003 proceedings) — describes handling of input data structures using "lazy initialization"
-
[http://scholar.sun.ac.za/bitstream/handle/10019.1/20335/redelinghuys_symbolic_2012.pdf?sequence=1 Symbolic String Execution] (Master Thesis) — describes String analysis
-
[https://code.google.com/p/green-solver/ Green Solver] SPF uses the Green Solver — Universal SAT/SMT solver
-
Coral and dReal — SPF uses Coral and dReal for solving non-linear floating-point constraints (email [email protected] for details)
-
Probabilistic SPF — SPF supports probabilistic symbolic execution using Latte and qCoral for model counting (email [email protected] for details)
-
[http://javapathfinder.sourceforge.net/events/JPF-workshop-050108/SymbolicJPF08.pdf Symbolic PathFinder] (presentation given at JPF workshop, MSR, ISSTA 2008)
-
[http://babelfish.arc.nasa.gov/trac/jpf/attachment/wiki/presentations/start/slides-pasareanu.pdf Symbolic Execution and SW Testing (uses SPF for illustration)] — Lecture Notes from Marktoberdorf Summerschool 2012
-
[http://javapathfinder.sourceforge.net/extensions/symbc/doc/index.html Old tool documentation]
-
[http://www.fujitsu.com/global/news/pr/archives/month/2010/20100112-02.html Fujitsu press announcement] released about using and extending Symbolic PathFinder ([wiki:projects/jpf-symbc]) for comprehensive testing of Java web applications
The old Mercurial repository is on http://babelfish.arc.nasa.gov/hg/jpf/jpf-symbc