{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:25:02Z","timestamp":1750307102687,"version":"3.41.0"},"reference-count":8,"publisher":"Association for Computing Machinery (ACM)","issue":"6","license":[{"start":{"date-parts":[[2012,11,27]],"date-time":"2012-11-27T00:00:00Z","timestamp":1353974400000},"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":[[2012,11,27]]},"abstract":"<jats:p>We present Abstract Pathfinder, an extension to the Java Pathfinder (JPF) verification tool-set that supports data abstraction to reduce the large data domains of a Java program to small, finite abstract domains, making the program more amenable to verification. We use data abstraction to compute an over-approximation of the original program in such a way that if a (safety) property is true in the abstracted program the property is also true in the original program. Our approach enhances JPF with an abstract interpreter and abstract state-matching mechanisms, together with a library of abstractions from which the user can pick which abstractions to use for a particular application. We discuss the details of our implementation together with some preliminary experiments with analyzing multi-threaded Java programs, where Abstract Pathfinder achieves significant time and memory savings as compared with plain JPF.<\/jats:p>","DOI":"10.1145\/2382756.2382794","type":"journal-article","created":{"date-parts":[[2012,11,29]],"date-time":"2012-11-29T15:02:27Z","timestamp":1354201347000},"page":"1-5","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Abstract pathfinder"],"prefix":"10.1145","volume":"37","author":[{"given":"Artem","family":"Khyzha","sequence":"first","affiliation":[{"name":"IMDEA Software Institute"}]},{"given":"Pavel","family":"Par\u00edzek","sequence":"additional","affiliation":[{"name":"Charles University in Prague"}]},{"given":"Corina S.","family":"P\u0103s\u0103reanu","sequence":"additional","affiliation":[{"name":"Carnegie Mellon\/NASA Ames"}]}],"member":"320","published-online":{"date-parts":[[2012,11,27]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/1965724.1965743"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-007-0044-z"},{"key":"e_1_2_1_3_1","volume-title":"Revamping TVLA: Making Parametric Shape Analysis Competitive. CAV","author":"Bogudlov I.","year":"2007","unstructured":"I. Bogudlov , T. Lev-Ami , T. W. Reps , and M. Sagiv . Revamping TVLA: Making Parametric Shape Analysis Competitive. CAV 2007 . I. Bogudlov, T. Lev-Ami, T. W. Reps, and M. Sagiv. Revamping TVLA: Making Parametric Shape Analysis Competitive. CAV 2007."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/337180.337234"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_1_6_1","volume-title":"Construction of Abstract State Graphs with PVS. In CAV","volume":"1254","author":"Graf S.","year":"1997","unstructured":"S. Graf and H. Saidi . Construction of Abstract State Graphs with PVS. In CAV 1997 , LNCS, vol. 1254 . S. Graf and H. Saidi. Construction of Abstract State Graphs with PVS. In CAV 1997, LNCS, vol. 1254."},{"key":"e_1_2_1_7_1","volume-title":"Combining Unit-level Symbolic Execution and System-level Concrete Execution for Testing NASA Software. ISSTA","author":"Pasareanu C. S.","year":"2008","unstructured":"C. S. Pasareanu , P. C. Mehlitz , D. H. Bushnell , K. Gundy-Burlet , M. R. Lowry , S. Person , and M. Pape . Combining Unit-level Symbolic Execution and System-level Concrete Execution for Testing NASA Software. ISSTA 2008 . C. S. Pasareanu, P. C. Mehlitz, D. H. Bushnell, K. Gundy-Burlet, M. R. Lowry, S. Person, and M. Pape. Combining Unit-level Symbolic Execution and System-level Concrete Execution for Testing NASA Software. ISSTA 2008."},{"key":"e_1_2_1_8_1","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\/."}],"container-title":["ACM SIGSOFT Software Engineering Notes"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2382756.2382794","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2382756.2382794","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T09:34:54Z","timestamp":1750239294000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2382756.2382794"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,11,27]]},"references-count":8,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2012,11,27]]}},"alternative-id":["10.1145\/2382756.2382794"],"URL":"https:\/\/doi.org\/10.1145\/2382756.2382794","relation":{},"ISSN":["0163-5948"],"issn-type":[{"type":"print","value":"0163-5948"}],"subject":[],"published":{"date-parts":[[2012,11,27]]},"assertion":[{"value":"2012-11-27","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}