wiki:papers/start

Related Publications

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

Notes:

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

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

"Differential Symbolic Execution". S. Person, M. Dwyer, S. Elbaum, C. S. Pasareanu, in Proceedings of FSE'08. http://portal.acm.org/citation.cfm?id=1453101.1453131

"Combining Unit-level Symbolic Execution and System-level Concrete Execution for Testing NASA Software", C. S. Pasareanu, P. C. Mehlitz, D. H. Bushnell, K. Gundy-Burlet, M. Lowry, S. Person, M. Pape, in Proceedings of ISSTA'08. http://ti.arc.nasa.gov/profile/pcorina/papers/fp047-pasareanu.pdf

"Symbolic Execution and Model Checking for Testing", Corina S. Pasareanu, Willem Visser, in Haifa Verification Conference 2007, LNCS 4899: 17-18 (IBM HVC Award). http://ti.arc.nasa.gov/profile/pcorina/papers/haifa07.pdf

"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 .

Verification of Networked Software

"Model Checking Distributed Systems by Combining Caching and Process Checkpointing." W. Leungwattanakit, C. Artho, M. Hagiya, Y. Tanabe, M. Yamamoto. ASE 2011, November 2011, Lawrence, USA. http://staff.aist.go.jp/c.artho/papers/checkpointing.pdf

"Cache-Based Model Checking of Networked Applications: From Linear to Branching Time". C. Artho, W. Leungwattanakit, M. Hagiya, Y. Tanabe, M. Yamamoto. ASE 2009, November 2009, Auckland, New Zealand. http://staff.aist.go.jp/c.artho/papers/ase-2009.pdf

"Efficient model checking of networked applications." C. Artho, W. Leungwattanakit, M. Hagiya, and Y. Tanabe. In Proc. TOOLS EUROPE 2008, volume 19 of LNBIP, pages 22–40, Zurich, Switzerland, 2008. Springer. http://staff.aist.go.jp/c.artho/papers/tools-2008.pdf

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

"Trust Your Model - Verifying Aerospace System Models with Java Pathfinder". Peter Mehlitz, Proc. IEEE Aerospace Conf. '08, Big Sky, MT, Mar. 1-8, 2008. http://ti.arc.nasa.gov/m/pub-archive/1402/1402%20(Mehlitz).pdf

"Hunting Application-Level Logical Errors". George Stergiopoulos, Bill Tsoumas, Dimitris Gritzalis. Proceedings of the 4th International Symposium on Engineering Secure Software and Sy­s­­tems (ESSOS-2012). Springer Lecture Notes in Computer Science, 2012, Volume 7159/2012

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

Papers from Darko Marinov's group http://mir.cs.illinois.edu/jpf/

"Test Generation through Programming in UDITA". M. Gligoric, T. Gvero, V. Jagannath, S. Khurshid, V. Kuncak, and D. Marinov. 32nd International Conference on Software Engineering (ICSE 2010), pages TO APPEAR, Cape Town, South Africa, May 2010. http://mir.cs.illinois.edu/~marinov/publications/GligoricETAL10UDITA.pdf

"MuTMuT: Efficient Exploration for Mutation Testing of Multithreaded Code". M. Gligoric, V. Jagannath, and D. Marinov. 3rd International Conference on Software Testing, Verification, and Validation (ICST 2010), pages TO APPEAR, Paris, France, April 2010. http://mir.cs.illinois.edu/~marinov/publications/GligoricETAL10MuTMuT.pdf

"Evaluating Ordering Heuristics for Dynamic Partial-Order Reduction Techniques". S. Lauterburg, R. K. Karmani, D. Marinov, and G. Agha. Fundamental Approach to Software Engineering (FASE 2010), pages TO APPEAR, Paphos, Cyprus, March 2010. http://mir.cs.illinois.edu/~marinov/publications/LauterburgETAL10DPORHeuristics.pdf

"A framework for state-space exploration of Java-based actor programs". S. Lauterburg, M. Dotta, D. Marinov, and G. Agha. 24th IEEE/ACM Conference on Automated Software Engineering (ASE 2009), pages 468-479, Auckland, New Zealand, November 2009. http://mir.cs.illinois.edu/~marinov/publications/LauterburgETAL09Basset.pdf

"Assertion checking in J-Sim simulation models of network protocols". A. Sobeih, M. d'Amorim, D. Marinov, and M. Viswanathan Simulation: Transactions of The Society for Modeling and Simulation International (SIMULATION), TO APPEAR (Accepted. To appear.).

"Optimizing generation of object graphs in Java PathFinder". M. Gligoric, T. Gvero, S. Lauterburg, D. Marinov and S. Khurshid. 2nd International Conference on Software Testing, Verification, and Validation (ICST 2009), Denver, Colorado, USA, April 2009. http://mir.cs.illinois.edu/~marinov/publications/GligoricETAL09OptimizingGeneration.pdf

"Delta execution for efficient state-space exploration of object-oriented programs". M. d'Amorim, S. Lauterburg, and D. Marinov. IEEE Transactions on Software Engineering (IEEE TSE), 34(5):597-613, September/October 2008. http://mir.cs.illinois.edu/~marinov/publications/dAmorimETAL08DeltaExecution.pdf

"Incremental state-space exploration for programs with dynamically allocated data". S. Lauterburg, A. Sobeih, D. Marinov, and M. Viswanathan. International Conference on Software Engineering (ICSE 2008), Leipzig, Germany, May 2008. http://mir.cs.illinois.edu/~marinov/publications/LauterburgETAL08IncrementalChecking.pdf

"State extensions for Java PathFinder". T. Gvero, M. Gligoric, S. Lauterburg, M. d'Amorim, D. Marinov, and S. Khurshid. International Conference on Software Engineering, Demo Papers (ICSE Demo 2008), Leipzig, Germany, May 2008. http://mir.cs.illinois.edu/~marinov/publications/GligoricETAL09OptimizingGeneration.pdf

"Delta execution for efficient state-space exploration of object-oriented programs". M. d'Amorim, S. Lauterburg, and D. Marinov. International Symposium on Software Testing and Analysis (ISSTA 2007), pages 50-60, London, UK, July 2007. http://mir.cs.illinois.edu/~marinov/publications/dAmorimETAL07DeltaExecution.pdf

"Delta execution for software reliability". Y. Zhou, D. Marinov, W. Sanders, C. Zilles, M. d'Amorim, S. Lauterburg, R. M. Lefever, and J. Tucek. Workshop on Hot Topics in System Dependability (HotDep 2007), Edinburgh, UK, June 2007. http://mir.cs.illinois.edu/~marinov/publications/ZhouETAL07DeltaExecution.pdf

"Optimized execution of deterministic blocks in Java PathFinder". M. d'Amorim, A. Sobeih, and D. Marinov. 8th International Conference on Formal Engineering Methods (ICFEM 2006), Macau, China, Nov. 2006. http://mir.cs.illinois.edu/~marinov/publications/dAmorimETAL06OptimizedDeterministicBlocks.pdf

"An empirical comparison of automated generation and classification techniques for object-oriented unit testing". M. d'Amorim, C. Pacheco, T. Xie, D. Marinov, and M. D. Ernst. 21st IEEE Conference on Automated Software Engineering (ASE 2006), pages 59-68, Tokyo, Japan, Sept. 2006. http://mir.cs.illinois.edu/~marinov/publications/dAmorimETAL06Symclat.pdf

Last modified 6 years ago Last modified on 02/26/2012 12:32:52 PM