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
omrsin/jpf-symbc
Module adapted as part of my master thesis: Symbolic Execution of Higher-order Functions in Big Data System. Presented to Prof. Guido Salvaneschi of the Technische Universität Darmstadt. The module should be used in conjunction with jpf-symspark found here https://github.com/omrsin/jpf-symspark
Java