JPF-SE: A Symbolic Execution Extension to Java Pathfinder

Abstract

We present JPF-SE, an extension to the Java PathFinder Model Checking framework (JPF) that enables the symbolic execution of Java programs. JPF{SE uses JPF to generate and explore symbolic execution paths and it uses of-the-shelf decision procedures to manipulate numeric constraints.


Related research categories:
(1) Symbolic Execution
(2) Empirical Studies
(3) Java

Go To Publications