Paper Info
Title
Method summaries for JPF
Abstract
Java Path nder (JPF) is a virtual machine executing Java byte- code that is able to perform model checking using backtracking execution. Due to backtracking, parts of a program may be ex- ecuted multiple times during model checking. Hence, we explore whether method summaries can be used to make JPF's model checking more efficient. We present the design and implementa- tion of dynamically generated summaries as an extension of JPF. While our summaries incur an overhead that outweighs the bene- ts in most cases, the approach shows promise in certain cases, in particular when stateless model checking is used. We also provide some results related to cases when our summaries are applicable that could provide guidance for future work within this eld.
Year
DOI
Venue
2019
10.1145/3364452.33644560
ACM SIGSOFT Software Engineering Notes
DocType
Volume
Issue
Journal
44
4
ISSN
Citations 
PageRank 
0163-5948
0
0.34
References 
Authors
0
2
Name
Order
Citations
PageRank
Lasse Berglund100.34
Cyrille Artho258844.46