{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:20:07Z","timestamp":1750306807227,"version":"3.41.0"},"reference-count":13,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2014,2,11]],"date-time":"2014-02-11T00:00:00Z","timestamp":1392076800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["SIGSOFT Softw. Eng. Notes"],"published-print":{"date-parts":[[2014,2,11]]},"abstract":"<jats:p>Habanero Java (HJ), a mid-level concurrent language, provides several correctness advantages if it is data race free: deadlock freedom, determinism, serialization, etc. An HJ program execution can only demonstrate data race freedom for one scheduling path, but the correctness property only holds if it is data race free for all paths. Verifying an HJ program with a tool such as Java Path Finder (JPF) for complete data race freedom is time and memory consuming because of the numerous JPF state expansions. This paper provides a small, stand-alone, alternative, HJ verification runtime (VR) that is more suited for verification in JPF. Additionally, this paper presents an alternative JPF scheduler that will explore only relevant HJ related scheduling paths in the VR. Finally, this paper shows state expansion results in JPF using HJ benchmarks with the HJ library, VR with and without the scheduler. The results indicate a reduction using the VR with the schedule when compared to the HJ runtime.<\/jats:p>","DOI":"10.1145\/2557833.2560582","type":"journal-article","created":{"date-parts":[[2014,2,18]],"date-time":"2014-02-18T14:08:32Z","timestamp":1392732512000},"page":"1-7","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["JPF verification of habanero Java programs"],"prefix":"10.1145","volume":"39","author":[{"given":"Peter","family":"Anderson","sequence":"first","affiliation":[{"name":"Brigham Young University, Provo, Utah"}]},{"given":"Brandon","family":"Chase","sequence":"additional","affiliation":[{"name":"Brigham Young University, Provo, Utah"}]},{"given":"Eric","family":"Mercer","sequence":"additional","affiliation":[{"name":"Brigham Young University, Provo, Utah"}]}],"member":"320","published-online":{"date-parts":[[2014,2,11]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103621.2103681"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2093157.2093165"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICST.2012.81"},{"key":"e_1_2_1_4_1","unstructured":"Habanero. Habanero multicore software research project. https:\/\/wiki.rice.edu\/confluence\/display\/HABANERO\/Habanero+Multicore+Software+Research+Project.  Habanero. Habanero multicore software research project. https:\/\/wiki.rice.edu\/confluence\/display\/HABANERO\/Habanero+Multicore+Software+Research+Project."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27940-9_22"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_9"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/SC.2010.7"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/PACT.2011.64"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1594835.1504214"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-29860-8_8"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31057-7_27"},{"key":"e_1_2_1_12_1","unstructured":"X10. X10: Performance and productivity at scale. http:\/\/x10-lang.org\/.  X10. X10: Performance and productivity at scale. http:\/\/x10-lang.org\/."},{"key":"e_1_2_1_13_1","doi-asserted-by":"crossref","unstructured":"T.\n       \n      Zirkel S.\n       \n      Siegel and \n      \n      \n      T.\n       \n      McClory\n    .\n      \n  \n   \n  Automated verification of Chapel programs using model checking and symbolic execution. In G. Brat N. Rungta and A. Venet editors NASA Formal Methods volume \n  7871\n   of \n  Lecture Notes in Computer Science pages \n  198\n  --\n  212\n  . \n  Springer Berlin Heidelberg 2013\n  .  T. Zirkel S. Siegel and T. McClory. Automated verification of Chapel programs using model checking and symbolic execution. In G. Brat N. Rungta and A. Venet editors NASA Formal Methods volume 7871 of Lecture Notes in Computer Science pages 198--212. Springer Berlin Heidelberg 2013.","DOI":"10.1007\/978-3-642-38088-4_14"}],"container-title":["ACM SIGSOFT Software Engineering Notes"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2557833.2560582","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2557833.2560582","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T07:34:58Z","timestamp":1750232098000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2557833.2560582"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,2,11]]},"references-count":13,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2014,2,11]]}},"alternative-id":["10.1145\/2557833.2560582"],"URL":"https:\/\/doi.org\/10.1145\/2557833.2560582","relation":{},"ISSN":["0163-5948"],"issn-type":[{"type":"print","value":"0163-5948"}],"subject":[],"published":{"date-parts":[[2014,2,11]]},"assertion":[{"value":"2014-02-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}