JPF-SE

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.


References in zbMATH (referenced in 10 articles )

Showing results 1 to 10 of 10.
Sorted by year (citations)

  1. Godefroid, Patrice; Sen, Koushik: Combining model checking and testing (2018)
  2. Lucas Cordeiro, Daniel Kroening, Peter Schrammel: Benchmarking of Java Verification Tools at the Software Verification Competition (SV-COMP) (2018) arXiv
  3. Matos, João; Garcia, João; Romano, Paolo: REAP: reporting errors using alternative paths (2014) ioport
  4. Brucker, Achim D.; Wolff, Burkhart: On theorem prover-based testing (2013)
  5. Fu, Xiang; Powell, Michael C.; Bantegui, Michael; Li, Chung-Chih: Simple linear string constraints (2013)
  6. Gaudel, Marie-Claude: Checking models, proving programs, and testing systems (2011) ioport
  7. van Gastel, Bernard; Lensink, Leonard; Smetsers, Sjaak; van Eekelen, Marko: Deadlock and starvation free reentrant readers-writers: a case study combining model checking with theorem proving (2011)
  8. Anand, Saswat; Păsăreanu, Corina S.; Visser, Willem: Symbolic execution with abstraction (2009) ioport
  9. Păsăreanu, Corina S.; Visser, Willem: A survey of new trends in symbolic execution for software testing and analysis (2009) ioport
  10. Anand, Saswat; Păsăreanu, Corina S.; Visser, Willem: JPF-SE: a symbolic execution extension to Java pathfinder (2007) ioport