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 11 articles )

Showing results 1 to 11 of 11.
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. Nguyen, Thanhvu; Weimer, Westley; Kapur, Deepak; Forrest, Stephanie: Connecting program synthesis and reachability: automatic program repair using test-input generation (2017)
  4. Matos, João; Garcia, João; Romano, Paolo: REAP: reporting errors using alternative paths (2014) ioport
  5. Brucker, Achim D.; Wolff, Burkhart: On theorem prover-based testing (2013)
  6. Fu, Xiang; Powell, Michael C.; Bantegui, Michael; Li, Chung-Chih: Simple linear string constraints (2013)
  7. Gaudel, Marie-Claude: Checking models, proving programs, and testing systems (2011) ioport
  8. 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)
  9. Anand, Saswat; Păsăreanu, Corina S.; Visser, Willem: Symbolic execution with abstraction (2009) ioport
  10. Păsăreanu, Corina S.; Visser, Willem: A survey of new trends in symbolic execution for software testing and analysis (2009) ioport
  11. Anand, Saswat; Păsăreanu, Corina S.; Visser, Willem: JPF-SE: a symbolic execution extension to Java pathfinder (2007) ioport