JPF-SE: A Symbolic Execution Extension to Java PathFinder

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 off-the-shelf decision procedures to manipulate numeric constraints.

• Type: Conference
• Year: 2007
• Where: TACAS
• Authors: Saswat Anand, Corina S. Pasareanu, Willem Visser
• Keywords: Algorithms, Jpf–se Uses Jpf, Symbolic Execution, Symbolic Execution Paths, TACAS 2007