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.
Keywords for this software
References in zbMATH (referenced in 8 articles )
Showing results 1 to 8 of 8.
- Matos, João; Garcia, João; Romano, Paolo: REAP: reporting errors using alternative paths (2014)
- Brucker, Achim D.; Wolff, Burkhart: On theorem prover-based testing (2013)
- Fu, Xiang; Powell, Michael C.; Bantegui, Michael; Li, Chung-Chih: Simple linear string constraints (2013)
- Gaudel, Marie-Claude: Checking models, proving programs, and testing systems (2011)
- 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)
- Anand, Saswat; Păsăreanu, Corina S.; Visser, Willem: Symbolic execution with abstraction (2009)
- Păsăreanu, Corina S.; Visser, Willem: A survey of new trends in symbolic execution for software testing and analysis (2009)
- Anand, Saswat; Păsăreanu, Corina S.; Visser, Willem: JPF-SE: a symbolic execution extension to Java pathfinder (2007)