{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,28]],"date-time":"2025-09-28T04:06:47Z","timestamp":1759032407740,"version":"3.41.0"},"reference-count":14,"publisher":"Association for Computing Machinery (ACM)","issue":"6","license":[{"start":{"date-parts":[[2017,1,5]],"date-time":"2017-01-05T00:00:00Z","timestamp":1483574400000},"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":[[2017,1,5]]},"abstract":"<jats:p>Some Java libraries have underdetermined specifications that allow more than one correct output for the same input, e.g., an output array may have its elements in any order. While such specifications have a number of advantages (e.g., a library can change while still satisfying the specification), the non-determinism inherent in underdetermined specifications can lead to failures in client code that erroneously assumes behaviors based on the library implementation instead of only the specification. Our recent work introduced the NonDex approach for detecting such erroneous assumptions by checking client code against models of library methods, which encode all behaviors allowed by the specifications<\/jats:p>\n          <jats:p>We present NonDex for JPF, which includes JPF models for 11 methods from the Java standard library (i.e., all methods that JPF supports from the current methods in Non-Dex). We use these models to systematically explore state spaces of 46 tests from student homework submissions. Our experiments show several interesting results, which provide new insights into the complexity of exploring the behaviors of code that uses underdetermined APIs and the structure of state spaces that arise in the exploration, and provide basis for future work on better detecting faults in tests that invoke underdetermined APIs as well as developing tool support for writing and maintaining more robust test suites<\/jats:p>","DOI":"10.1145\/3011286.3011295","type":"journal-article","created":{"date-parts":[[2017,1,6]],"date-time":"2017-01-06T13:30:07Z","timestamp":1483709407000},"page":"1-5","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Exploring Underdetermined Specifications using Java PathFinder"],"prefix":"10.1145","volume":"41","author":[{"given":"Alex","family":"Gyori","sequence":"first","affiliation":[{"name":"University of Illinois at Urbana-Champaign"}]},{"given":"Ben","family":"Lambeth","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign"}]},{"given":"Sarfraz","family":"Khurshid","sequence":"additional","affiliation":[{"name":"The University of Texas at Austin"}]},{"given":"Darko","family":"Marinov","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign"}]}],"member":"320","published-online":{"date-parts":[[2017,1,5]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"Ben Lambeth's GitHub. https:\/\/github.com\/azy2.  Ben Lambeth's GitHub. https:\/\/github.com\/azy2."},{"key":"e_1_2_1_2_1","unstructured":"Checkstyle Pull Request. https:\/\/github.com\/checkstyle\/checkstyle\/pull\/3393.  Checkstyle Pull Request. https:\/\/github.com\/checkstyle\/checkstyle\/pull\/3393."},{"key":"e_1_2_1_3_1","unstructured":"Class#getDeclaredFields Javadoc. https:\/\/docs.oracle.com\/javase\/8\/docs\/api\/java\/lang\/Class.html#getDeclaredFields--.  Class#getDeclaredFields Javadoc. https:\/\/docs.oracle.com\/javase\/8\/docs\/api\/java\/lang\/Class.html#getDeclaredFields--."},{"key":"e_1_2_1_4_1","unstructured":"Class#getFields in Java PathFinder. http:\/\/babelfish.arc.nasa.gov\/hg\/jpf\/jpf-core\/file\/0069194b1048\/src\/peers\/gov\/nasa\/jpf\/vm\/JPF java lang Class.java#l580.  Class#getFields in Java PathFinder. http:\/\/babelfish.arc.nasa.gov\/hg\/jpf\/jpf-core\/file\/0069194b1048\/src\/peers\/gov\/nasa\/jpf\/vm\/JPF java lang Class.java#l580."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1181775.1181787"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2950290.2983932"},{"key":"e_1_2_1_7_1","unstructured":"HashSet Javadoc. https:\/\/docs.oracle.com\/javase\/8\/docs\/api\/java\/util\/HashSet.html.  HashSet Javadoc. https:\/\/docs.oracle.com\/javase\/8\/docs\/api\/java\/util\/HashSet.html."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2635868.2635917"},{"key":"e_1_2_1_9_1","unstructured":"JUnit 4.11 - What's new? Test execution order. http:\/\/randomallsorts.blogspot.com\/2012\/12\/junit-411-whats-new-test-execution-order.html.  JUnit 4.11 - What's new? Test execution order. http:\/\/randomallsorts.blogspot.com\/2012\/12\/junit-411-whats-new-test-execution-order.html."},{"key":"e_1_2_1_10_1","volume-title":"Seminumerical algorithms, the art of computer programming","author":"Knuth D.","year":"1997","unstructured":"D. Knuth . Seminumerical algorithms, the art of computer programming , vol. 2 1997 . D. Knuth. Seminumerical algorithms, the art of computer programming, vol. 2 1997."},{"key":"e_1_2_1_11_1","unstructured":"NonDex Source Code. https:\/\/github.com\/TestingResearchIllinois\/NonDex.  NonDex Source Code. https:\/\/github.com\/TestingResearchIllinois\/NonDex."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-008-0070-5"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/356689.356692"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICST.2016.40"}],"container-title":["ACM SIGSOFT Software Engineering Notes"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3011286.3011295","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3011286.3011295","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T19:05:28Z","timestamp":1750273528000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3011286.3011295"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,1,5]]},"references-count":14,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2017,1,5]]}},"alternative-id":["10.1145\/3011286.3011295"],"URL":"https:\/\/doi.org\/10.1145\/3011286.3011295","relation":{},"ISSN":["0163-5948"],"issn-type":[{"type":"print","value":"0163-5948"}],"subject":[],"published":{"date-parts":[[2017,1,5]]},"assertion":[{"value":"2017-01-05","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}