{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,21]],"date-time":"2026-01-21T16:15:22Z","timestamp":1769012122879,"version":"3.49.0"},"publisher-location":"Cham","reference-count":39,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031572487","type":"print"},{"value":"9783031572494","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,4,5]],"date-time":"2024-04-05T00:00:00Z","timestamp":1712275200000},"content-version":"vor","delay-in-days":95,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We give an account of JPF\u2019s current architecture as it has evolved over the last 20 years. Key changes include a modular, extensible design, and Java 11 support.<\/jats:p><jats:p>Java 11 brought with it fundamental changes in the language and its runtime, in particular, a new modular library system, different compilation of string expressions to bootstrap methods, and changes in many internal interfaces that allow access to the loaded code and the virtual machine state. These changes required numerous adaptations in JPF to ensure a successful compilation and correct behavior under Java 11.<\/jats:p>","DOI":"10.1007\/978-3-031-57249-4_1","type":"book-chapter","created":{"date-parts":[[2024,4,4]],"date-time":"2024-04-04T07:02:35Z","timestamp":1712214155000},"page":"3-22","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["JPF: From 2003 to 2023"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3656-1614","authenticated-orcid":false,"given":"Cyrille","family":"Artho","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0714-7446","authenticated-orcid":false,"given":"Pavel","family":"Par\u00edzek","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0004-3811-6591","authenticated-orcid":false,"given":"Daohan","family":"Qu","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0007-2086-4542","authenticated-orcid":false,"given":"Varadraj","family":"Galgali","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6669-6520","authenticated-orcid":false,"given":"Pu","family":"Yi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,4,5]]},"reference":[{"key":"1_CR1","doi-asserted-by":"crossref","unstructured":"Willem Visser, Klaus Havelund, Guillaume Brat, SeungJoon Park, and Flavio Lerda. Model checking programs. Automated Software Engineering, 10(2):203\u2013232, 2003.","DOI":"10.1023\/A:1022920129859"},{"key":"1_CR2","doi-asserted-by":"crossref","unstructured":"Cyrille Artho and Willem Visser. Java Pathfinder at SV-COMP 2019 (competition contribution). In Dirk Beyer, Marieke Huisman, Fabrice Kordon, and Bernhard Steffen, editors, Tools and Algorithms for the Construction and Analysis of Systems, pages 224\u2013228, Cham, 2019. Springer International Publishing.","DOI":"10.1007\/978-3-030-17502-3_18"},{"key":"1_CR3","unstructured":"G.\u00a0Holzmann. The SPIN Model Checker. Addison-Wesley, 2004."},{"key":"1_CR4","doi-asserted-by":"crossref","unstructured":"Corina\u00a0S. P\u01ces\u01cereanu and Neha Rungta. Symbolic PathFinder: Symbolic execution of Java bytecode. In Proceedings of the 25th IEEE\/ACM International Conference on Automated Software Engineering, pages 179\u2013180, 2010.","DOI":"10.1145\/1858996.1859035"},{"key":"1_CR5","unstructured":"James Gosling, Bill Joy, Guy Steele, Gilad Bracha, Alex Buckley, and Daniel Smith. The Java Language Specification, Java SE 11 Edition. Oracle, 2018."},{"key":"1_CR6","doi-asserted-by":"crossref","unstructured":"Matt Walker, Parssa Khazra, Anto Nanah\u00a0Ji, Hongru Wang, and Franck van Breugel. jpf-logic: a framework for checking temporal logic properties of Java code. ACM SIGSOFT Software Engineering Notes, 48(1):32\u201336, 2023.","DOI":"10.1145\/3573074.3573083"},{"key":"1_CR7","doi-asserted-by":"crossref","unstructured":"Klaus Havelund. Java PathFinder, a translator from Java to Promela. In Theoretical and Practical Aspects of SPIN Model Checking: 5th and 6th International SPIN Workshops Trento, Italy, July 5, 1999 Toulouse, France, September 21 and 24, 1999 Proceedings 5, pages 152\u2013152. Springer, 1999.","DOI":"10.1007\/3-540-48234-2_11"},{"key":"1_CR8","unstructured":"Martin Fowler and Matthew Foemmel. Continuous integration. http:\/\/www.martinfowler.com\/articles\/continuousIntegration.html, 2006."},{"key":"1_CR9","doi-asserted-by":"crossref","unstructured":"Cyrille Artho, Viktor Schuppan, Armin Biere, Pascal Eugster, Marcel Baur, and Boris Zweim\u00fcller. JNuke: Efficient dynamic analysis for Java. In Rajeev Alur and Doron\u00a0A. Peled, editors, Computer Aided Verification, pages 462\u2013465, Berlin, Heidelberg, 2004. Springer Berlin Heidelberg.","DOI":"10.1007\/978-3-540-27813-9_37"},{"key":"1_CR10","unstructured":"Niels\u00a0HM Aan\u00a0de Brugh, Viet\u00a0Yen Nguyen, and Theo\u00a0C Ruys. Moonwalker: Verification of .NET programs. In Tools and Algorithms for the Construction and Analysis of Systems: 15th International Conference, TACAS 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings 15, pages 170\u2013173. Springer, 2009."},{"key":"1_CR11","doi-asserted-by":"crossref","unstructured":"Nicholas Nethercote and Julian Seward. Valgrind: a framework for heavyweight dynamic binary instrumentation. ACM Sigplan notices, 42(6):89\u2013100, 2007.","DOI":"10.1145\/1273442.1250746"},{"key":"1_CR12","unstructured":"Cristian Cadar, Daniel Dunbar, Dawson\u00a0R Engler, et\u00a0al. Klee: Unassisted and automatic generation of high-coverage tests for complex systems programs. In OSDI, volume\u00a08, pages 209\u2013224, 2008."},{"key":"1_CR13","doi-asserted-by":"crossref","unstructured":"Chris Lattner and Vikram Adve. LLVM: A compilation framework for lifelong program analysis & transformation. In International symposium on code generation and optimization, 2004. CGO 2004., pages 75\u201386. IEEE, 2004.","DOI":"10.1109\/CGO.2004.1281665"},{"key":"1_CR14","doi-asserted-by":"crossref","unstructured":"Thomas Ball and Sriram\u00a0K Rajamani. The SLAM toolkit. In Proceedings of CAV 2001 (13th Conference on Computer Aided Verification), volume 2102, pages 260\u2013264, 2000.","DOI":"10.1007\/3-540-44585-4_25"},{"key":"1_CR15","unstructured":"Daniel Kroening and Michael Tautschnig. CBMC\u2013C bounded model checker: (competition contribution). In Tools and Algorithms for the Construction and Analysis of Systems: 20th International Conference, TACAS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014. Proceedings 20, pages 389\u2013391. Springer, 2014."},{"key":"1_CR16","doi-asserted-by":"crossref","unstructured":"Les Hatton. Safer language subsets: an overview and a case history, MISRA C. Information and Software Technology, 46(7):465\u2013472, 2004.","DOI":"10.1016\/j.infsof.2003.09.016"},{"key":"1_CR17","doi-asserted-by":"crossref","unstructured":"Cormac Flanagan and Stephen\u00a0N. Freund. The RoadRunner dynamic analysis framework for concurrent programs. In Sorin Lerner and Atanas Rountev, editors, Proceedings of the 9th ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering, PASTE\u201910, Toronto, Ontario, Canada, June 5-6, 2010, pages 1\u20138. ACM, 2010.","DOI":"10.1145\/1806672.1806674"},{"key":"1_CR18","doi-asserted-by":"crossref","unstructured":"Lukas Marek, Yudi Zheng, Danilo Ansaloni, Aibek Sarimbekov, Walter Binder, Petr Tuma, and Zhengwei Qi. Java bytecode instrumentation made easy: The DiSL framework for dynamic program analysis. In Ranjit Jhala and Atsushi Igarashi, editors, Programming Languages and Systems - 10th Asian Symposium, APLAS 2012, Kyoto, Japan, December 11-13, 2012. Proceedings, volume 7705 of Lecture Notes in Computer Science, pages 256\u2013263. Springer, 2012.","DOI":"10.1007\/978-3-642-35182-2_18"},{"key":"1_CR19","doi-asserted-by":"crossref","unstructured":"Andrej \u010cizm\u00e1rik and Pavel Par\u00edzek. SharpDetect: Dynamic analysis framework for C#\/.NET programs. In Jyotirmoy Deshmukh and Dejan Nickovic, editors, Runtime Verification - 20th International Conference, RV 2020, Los Angeles, CA, USA, October 6-9, 2020, Proceedings, volume 12399 of Lecture Notes in Computer Science, pages 298\u2013309. Springer, 2020.","DOI":"10.1007\/978-3-030-60508-7_16"},{"key":"1_CR20","doi-asserted-by":"crossref","unstructured":"Kyle Storey, Eric Mercer, and Pavel Parizek. A sound dynamic partial order reduction engine for Java Pathfinder. ACM SIGSOFT Software Engineering Notes, 44(4):15\u201315, 2021.","DOI":"10.1145\/3364452.3364457"},{"key":"1_CR21","doi-asserted-by":"crossref","unstructured":"Jeremy Manson, William Pugh, and Sarita\u00a0V Adve. The Java memory model. ACM SIGPLAN Notices, 40(1):378\u2013391, 2005.","DOI":"10.1145\/1047659.1040336"},{"key":"1_CR22","unstructured":"Huafeng Jin, Tuba Yavuz-Kahveci, and Beverly\u00a0A Sanders. Java memory model-aware model checking. In Tools and Algorithms for the Construction and Analysis of Systems: 18th International Conference, TACAS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24\u2013April 1, 2012. Proceedings 18, pages 220\u2013236. Springer, 2012."},{"key":"1_CR23","doi-asserted-by":"crossref","unstructured":"Nastaran Shafiei and Peter Mehlitz. Extending JPF to verify distributed systems. ACM SIGSOFT Software Engineering Notes, 39(1):1\u20135, 2014.","DOI":"10.1145\/2557833.2560577"},{"key":"1_CR24","doi-asserted-by":"crossref","unstructured":"Cyrille Artho, Kuniyasu Suzaki, Masami Hagiya, Watcharin Leungwattanakit, Richard Potter, Eric Platon, Yoshinori Tanabe, Franz Weitl, and Mitsuharu Yamamoto. Using checkpointing and virtualization for fault injection. IJNC, 5(2):347\u2013372, 2015.","DOI":"10.15803\/ijnc.5.2_347"},{"key":"1_CR25","doi-asserted-by":"crossref","unstructured":"Nastaran Shafiei and Franck\u00a0van Breugel. Automatic handling of native methods in Java PathFinder. In Proceedings of the 2014 International SPIN Symposium on Model Checking of Software, pages 97\u2013100, 2014.","DOI":"10.1145\/2632362.2632363"},{"key":"1_CR26","doi-asserted-by":"crossref","unstructured":"Watcharin Leungwattanakit, Cyrille Artho, Masami Hagiya, Yoshinori Tanabe, Mitsuharu Yamamoto, and Koichi Takahashi. Modular software model checking for distributed systems. IEEE Transactions on Software Engineering, 40(5):483\u2013501, 2013.","DOI":"10.1109\/TSE.2013.49"},{"key":"1_CR27","unstructured":"Tim Lindholm, Frank Yellin, Gilad Bracha, and Alex Buckley. The Java Virtual Machine Specification. Addison-Wesley, 2013."},{"key":"1_CR28","unstructured":"Alan Bateman, Alex Buckley, Jonathon Gibbons, and Mark Reinhold. JEP 261: The module system. https:\/\/openjdk.org\/jeps\/261, 2014."},{"key":"1_CR29","unstructured":"Oracle. Class CallSite. https:\/\/docs.oracle.com\/en\/java\/javase\/11\/docs\/api\/java.base\/java\/lang\/invoke\/CallSite.html, 2018."},{"key":"1_CR30","unstructured":"Alex Buckley and Mark Reinhold. JEP 396: Strongly encapsulate JDK internals by default. https:\/\/openjdk.org\/jeps\/396, 2020."},{"key":"1_CR31","unstructured":"Alex Buckley and Mark Reinhold. JEP 403: Strongly encapsulate JDK internals. https:\/\/openjdk.org\/jeps\/403, 2021."},{"key":"1_CR32","unstructured":"Brent Christian and Xueming Shen. JEP 254: Compact strings. https:\/\/openjdk.org\/jeps\/254, 2014."},{"key":"1_CR33","doi-asserted-by":"crossref","unstructured":"Wing Lam, Reed Oei, August Shi, Darko Marinov, and Tao Xie. iDFlakies: A framework for detecting and partially classifying flaky tests. In 2019 12th IEEE Conference on Software Testing, Validation and Verification (ICST), pages 312\u2013322, 2019.","DOI":"10.1109\/ICST.2019.00038"},{"key":"1_CR34","doi-asserted-by":"crossref","unstructured":"Alex Gyori, August Shi, Farah Hariri, and Darko Marinov. Reliable testing: Detecting state-polluting tests to prevent test dependency. In Proceedings of the 2015 International Symposium on Software Testing and Analysis, ISSTA 2015, page 223\u2013233, New York, NY, USA, 2015. Association for Computing Machinery.","DOI":"10.1145\/2771783.2771793"},{"key":"1_CR35","doi-asserted-by":"crossref","unstructured":"Pu\u00a0Yi, Anjiang Wei, Wing Lam, Tao Xie, and Darko Marinov. Finding polluter tests using Java PathFinder. SIGSOFT Softw. Eng. Notes, 46(3):37\u201341, 2021.","DOI":"10.1145\/3468744.3468756"},{"key":"1_CR36","doi-asserted-by":"crossref","unstructured":"Robert\u00a0R Schaller. Moore\u2019s law: past, present and future. IEEE spectrum, 34(6):52\u201359, 1997.","DOI":"10.1109\/6.591665"},{"key":"1_CR37","doi-asserted-by":"crossref","unstructured":"Laszlo\u00a0B Kish. End of Moore\u2019s law: thermal (noise) death of integration in micro and nano electronics. Physics Letters A, 305(3-4):144\u2013149, 2002.","DOI":"10.1016\/S0375-9601(02)01365-8"},{"key":"1_CR38","doi-asserted-by":"crossref","unstructured":"M.\u00a0Hsueh, T.\u00a0Tsai, and R.\u00a0Iyer. Fault injection techniques and tools. IEEE Computer, 30(4):75\u201382, 1997.","DOI":"10.1109\/2.585157"},{"key":"1_CR39","unstructured":"The JPF Team. Writing JPF tests. https:\/\/github.com\/javapathfinder\/jpf-core\/wiki\/Writing-JPF-tests, 2023."}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-57249-4_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,15]],"date-time":"2024-11-15T17:16:08Z","timestamp":1731690968000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-57249-4_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031572487","9783031572494"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-57249-4_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"5 April 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 April 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2024\/conferences\/tacas\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"159","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"53","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"16","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"33% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"10","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}