{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:16:09Z","timestamp":1763468169347,"version":"3.41.0"},"reference-count":9,"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>Model checkers like Java PathFinder (JPF) often have to combat the state space explosion problem. One solution adopted to tackle this problem is to abstract away parts of the system, e. g., to model complex library classes at a higher level of abstraction. The model classes have the same interface as the actual library classes but exhibit reduced be- haviour and state. Writing such model classes is both error prone and time consuming. In this paper we propose a tool that can automatically derive a model class from the original class. To achieve this goal, the tool uses different algorithms, including slicing and value generation, each yielding a model class with different behaviour and state.<\/jats:p>","DOI":"10.1145\/2557833.2560572","type":"journal-article","created":{"date-parts":[[2014,2,18]],"date-time":"2014-02-18T14:08:32Z","timestamp":1392732512000},"page":"1-5","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":10,"title":["Automated generation of model classes for Java PathFinder"],"prefix":"10.1145","volume":"39","author":[{"given":"Matteo","family":"Ceccarello","sequence":"first","affiliation":[{"name":"University of Padua, Padova, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Oksana","family":"Tkachuk","sequence":"additional","affiliation":[{"name":"SGT, Inc.\/NASA Ames Research Center, Moffett Field, California"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2014,2,11]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2009.43"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2382756.2382796"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/1592955"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2011.6100131"},{"volume-title":"Automatic on-demand delegation of calls in Java PathFinder","year":"2013","author":"Shafiei N.","key":"e_1_2_1_5_1"},{"key":"e_1_2_1_6_1","first-page":"121","article-title":"A survey of program slicing techniques","volume":"3","author":"Tip F.","year":"1995","journal-title":"Journal Of Programming Languages"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/940071.940097"},{"volume-title":"jpf-concurrent: An extension of java PathFinder for java. util. concurrent. arXiv preprint 1205.0042","year":"2012","author":"Ujma M.","key":"e_1_2_1_8_1"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1022920129859"}],"container-title":["ACM SIGSOFT Software Engineering Notes"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2557833.2560572","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2557833.2560572","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.2560572"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,2,11]]},"references-count":9,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2014,2,11]]}},"alternative-id":["10.1145\/2557833.2560572"],"URL":"https:\/\/doi.org\/10.1145\/2557833.2560572","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"}}]}}