State extensions for java pathfinder

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

State extensions for java pathfinder

Full text

Pdf (118 KB)

Source

International Conference on Software Engineering archive
Proceedings of the 30th international conference on Software engineering table of contents

Leipzig, Germany

SESSION: Verification & validation table of contents

Pages 863-866

Year of Publication: 2008

ISBN:978-1-60558-079-1

Authors

Tihomir Gvero	University of Belgrade, Belgrade, Serbia
Milos Gligoric	University of Belgrade, Belgrade, Serbia
Steven Lauterburg	University of Illinois, Urbana, IL, USA
Marcelo d'Amorim	University of Illinois, Urbana, IL, USA
Darko Marinov	University of Illinois, Urbana, IL, USA
Sarfraz Khurshid	University of Texas at Austin

Sponsors

ACM: Association for Computing Machinery
SIGSOFT: ACM Special Interest Group on Software Engineering

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 14, Downloads (12 Months): 116, Citation Count: 0

Additional Information:

abstract references index terms collaborative colleagues

Tools and Actions:	Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/1368088.1368224 What is a DOI?

ABSTRACT

Java PathFinder (JPF) is an explicit-state model checker for Java programs. JPF implements a backtrackable Java Virtual Machine (JVM) that provides non-deterministic choices and control over thread scheduling. JPF is itself implemented in Java and runs on top of a host JVM. JPF represents the JVM state of the program being checked and performs three main operations on this state representation: bytecode execution, state backtracking, and state comparison. This paper summarizes four extensions that we have developed to the JPF state representation and operations. One extension provides a new functionality to JPF, and three extensions improve performance of JPF in various scenarios. Some of our code has already been included in publicly available JPF.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	Java PathFinder web site. http://javapathfinder.sourceforge.net.
	2	S. Anand, C. S. Pasareanu, and W. Visser. JPF-SE: A symbolic execution extension to Java PathFinder. In TACAS, 2007.
	3	Marcelo D'Amorim , Darko Marinov, Efficient explicit-state model checking for programs with dynamically allocated data, University of Illinois at Urbana-Champaign, Champaign, IL, 2007
	4	Marcelo d'Amorim , Steven Lauterburg , Darko Marinov, Delta execution for efficient state-space exploration of object-oriented programs, Proceedings of the 2007 international symposium on Software testing and analysis, July 09-12, 2007, London, United Kingdom [doi>10.1145/1273463.1273472]
	5	M. d'Amorim, A. Sobeih, and D. Marinov. Optimized execution of deterministic blocks in Java PathFinder. In ICFEM, 2006.
	6	Willem Visser , Klaus Havelund , Guillaume Brat , Seungjoon Park , Flavio Lerda, Model Checking Programs, Automated Software Engineering, v.10 n.2, p.203-232, April 2003 [doi>10.1023/A:1022920129859]