JPF Related Papers

JPF has been both a research target and a system in use for a number of years. A broad collection of papers and reports is available, including the following (incomplete) list

Please Note - some of the older papers now have mostly historical relevance. JPF has undergone a lot of changes since 2000. If you need more recent information, esp. about the design and usage of current JPF versions, please consult the documentation on the web site.

Core Papers

"Model Checking Programs". W. Visser, K. Havelund, G. Brat, S. Park and F. Lerda. Automated Software Engineering Journal.Volume 10, Number 2, April 2003. http://ti.arc.nasa.gov/people/wvisser/ase00FinalJournal.pdf

"Addressing Dynamic Issues of Program Model Checking". F. Lerda and W. Visser. Proccedings of SPIN2001. Toronto, May 2001. http://ti.arc.nasa.gov/people/wvisser/spin01.ps.gz

Testing and Symbolic Execution

"Generalized Symbolic Execution for Model Checking and Testing". S. Khurshid, C. S. Pasareanu and W. Visser. Proceedings of TACAS 2003. Warsaw, Poland, April 2003. http://ti.arc.nasa.gov/people/wvisser/tacas-symex.ps

"Test Input Generation with Java PathFinder ". W. Visser, C. Pasareanu, S. Khurshid. Proceedings of ISSTA 2004. Boston, MA, July 2004. http://ti.arc.nasa.gov/people/wvisser/issta-visser.pdf

"Verification of Java Programs Using Symbolic Execution and Invariant Generation". C. Pasareanu and W. Visser . Proceedings of SPIN 2004. Barcelona, Spian, April 2004 . LNCS 2989. http://ti.arc.nasa.gov/people/wvisser/spin04.ps

"Experiments with Test Case Generation and Runtime Analysis". C. Artho, D. Drusinsky, A. Goldberg, K. Havelund, M. Lowry, C. Pasareanu, G. Rosu, W. Visser. Proceedings of Abstract State Machines 2003 . Taormina, Italy, March 2003. LNCS 2589. http://ti.arc.nasa.gov/people/wvisser/asm03-invited.pdf

Heuristic Search

"Heuristics for Model Checking Java Programs ". A. Groce and W. Visser. International Journal on Software Tools for Technology Transfer (STTT). Volume 6, Number 4, December 2004. http://ti.arc.nasa.gov/people/wvisser/stttheur.ps

"Model Checking Java Programs using Structural Heuristics" . A. Groce and W. Visser. Proceedings of ISSTA 2002. Rome, Italy. July 2002. http://ti.arc.nasa.gov/people/wvisser/issta02_paper.ps

"Heuristic Model Checking for Java Programs". A. Groce and W. Visser. Proceedings of SPIN 2002. Grenoble, France. April 2002 .

Explaining Counter Examples

"What Went Wrong: Explaining Counterexamples". A. Groce and W. Visser. Proceedings of SPIN 2003. Portland, Oregon. May 2003.

Using Java PathFinder

"Verifying Time Partitioning in the DEOS Scheduling Kernel" . J. Penix, W. Visser. S. Park, C. Pasareanu, E. Engstrom, A. Larson and N. Weininger. Formal Methods in Systems Design Journal. Volume 26, Number 2, March 2005. http://ti.arc.nasa.gov/people/wvisser/final-Penix-Visser.ps

"Experimental Evaluation of Verification and Validation Tools on Martian Rover Software". G. Brat, D. Drusinsky, D. Giannakopoulou, A. Goldberg, K. Havelund, M. Lowry, C. Pasareanu, A. Venet, R. Washington and W. Visser. Formal Methods in Systems Design Journal . Volume 25, Number 2-3, September 2004. http://ti.arc.nasa.gov/people/wvisser/fmsdjournal.pdf

"Model Checking Multi-Agent Programs with CASP" . R. Bordini, M. Fisher, C. Pardavila, W. Visser, M. Wooldridge . Proceedings of CAV 2003. Boulder, Colorado, July 2003 . LNCS 2725. http://ti.arc.nasa.gov/people/wvisser/agentscav.ps

"Assume-guarantee Verification of Source Code with Design-Level Assumptions". D. Giannakopoulou, C. S. Pasareanu, J. M. Cobleigh. Proceedings of the 26th International Conference on Software Engineering (ICSE). Edinburgh, Scotland. May 2004. http://ti.arc.nasa.gov/people/wvisser/icse04.pdf

"Model Checking Real Time Java Using JavaPathfinder", G. Lindstrom, P. Mehlitz and W. Visser, Proceedings of the Third International Symposium on Automated Technology for Verification and Analysis (ATVA), October 2005

Misc

"Program Model Checking - A Practitioners Guide", Masoud Mansouri-Samani, John Penix, Lawrence Markosian et al, Software Assurance Research Program (SARP), NASA IV&V publication 2007 http://sarpresults.ivv.nasa.gov/DownloadFile/59/17/Practitioner's Guidebook_20070427 _final.pdf

"Program Model Checking as a New Trend". K. Havelund and W. Visser. International Journal on Software Tools for Technology Transfer (STTT). Volume 4, Number 1, October 2002. http://ti.arc.nasa.gov/people/wvisser/sttt-spin2000.pdf

"Finding Feasible Abstract Counter-Examples" . C. Pasareanu, M. Dwyer and W. Visser. International Journal on Software Tools for Technology Transfer (STTT) Volume 5, Number 1, November 2003. http://ti.arc.nasa.gov/people/wvisser/tacas_sttt01.ps

"Combining Static Analysis and Model Checking for Software Analysis". G. Brat and W. Visser. Proceedings of ASE2001. San Diego, November 2001. http://ti.arc.nasa.gov/people/wvisser/mcsa.ps.gz

"Applying Predicate Abstraction to Model Check Object-Oriented Programs". W. Visser, S. Park and J. Penix. 3rd ACM SIGSOFT Workshop on Formal Methods in Software Practice. August 2000. http://ti.arc.nasa.gov/people/wvisser/fmsp00.ps.gz

"Model Checking Java Programs Using Java PathFinder". K. Havelund, T. Pressburger. International Journal on Software Tools for Technology Transfer (STTT) 2(4), April 2000. Special issue containing selected submissions for the 4'th SPIN workshop, Paris, November 1998 http://www.havelund.com/Publications/jpf-sttt.ps.Z

"Java PathFinder, A Translator from Java to Promela". K. Havelund. Theoretical and Practical Aspects of SPIN Model Checking, Toulouse, France, September, 1999 http://www.havelund.com/Publications/jpf1-spin-99.pdf

"Applying Model Checking in Java Verification". K. Havelund, J. Skakkebaek. Proceedings of 6th SPIN Workshop in connection with FM99 Toulouse http://www.havelund.com/Publications/jpf-fm99.ps.Z

"Java PathFinder User Guide". K. Havelund. Unpublished Report, 1999 http://www.havelund.com/Publications/jpf-manual.ps.Z

"Java PathFinder, A Translator from Java to Promela". K. Havelund and T. Pressburger. Unpublished Report, 1998. http://www.havelund.com/Publications/jpf1-report-99.pdf