{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:20:06Z","timestamp":1750306806362,"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>We present our ongoing effort to implement predicate abstraction in Abstract Pathfinder, which is an extension of Java Pathfinder. Our approach builds upon existing abstraction techniques that have been proposed mainly for low-level programs in C. We support predicates over variables having numerical data types. The main challenges that we have addressed include (1) the design of the predicate language, (2) support for arrays, (3) finding predicates affected by a given statement, (4) aliasing between variables, (5) propagating values of predicates over method call boundaries, and (6) computing weakest preconditions for complex predicates. We describe our solution to these challenges and selected details about the implementation. We also discuss our future plans and research ideas.<\/jats:p>","DOI":"10.1145\/2557833.2560573","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":2,"title":["Predicate abstraction in Java Pathfinder"],"prefix":"10.1145","volume":"39","author":[{"given":"Jakub","family":"Daniel","sequence":"first","affiliation":[{"name":"Charles University in Prague"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pavel","family":"Par\u00edzek","sequence":"additional","affiliation":[{"name":"Charles University in Prague"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Corina S.","family":"P\u0103s\u0103reanu","sequence":"additional","affiliation":[{"name":"Carnegie Mellon\/NASA Ames"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2014,2,11]]},"reference":[{"doi-asserted-by":"publisher","key":"e_1_2_1_1_1","DOI":"10.1007\/s10009-008-0090-1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_2_1","DOI":"10.1145\/378795.378846"},{"doi-asserted-by":"publisher","key":"e_1_2_1_3_1","DOI":"10.5555\/1296691.1296695"},{"doi-asserted-by":"publisher","key":"e_1_2_1_4_1","DOI":"10.5555\/647769.734089"},{"doi-asserted-by":"publisher","key":"e_1_2_1_5_1","DOI":"10.5555\/647766.733618"},{"doi-asserted-by":"publisher","key":"e_1_2_1_6_1","DOI":"10.1109\/32.588521"},{"unstructured":"Java Pathfinder: framework for verification of Java programs. http:\/\/babelfish.arc.nasa.gov\/trac\/jpf\/.  Java Pathfinder: framework for verification of Java programs. http:\/\/babelfish.arc.nasa.gov\/trac\/jpf\/.","key":"e_1_2_1_7_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_8_1","DOI":"10.1145\/2382756.2382794"},{"doi-asserted-by":"publisher","key":"e_1_2_1_9_1","DOI":"10.1145\/1858996.1859035"}],"container-title":["ACM SIGSOFT Software Engineering Notes"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2557833.2560573","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2557833.2560573","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.2560573"}},"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.2560573"],"URL":"https:\/\/doi.org\/10.1145\/2557833.2560573","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"}}]}}