{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,4]],"date-time":"2026-10-04T11:06:13Z","timestamp":1791111973834,"version":"4.1.0"},"reference-count":55,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2005,3,1]],"date-time":"2005-03-01T00:00:00Z","timestamp":1109635200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Method Syst Des"],"published-print":{"date-parts":[[2005,3]]},"DOI":"10.1007\/s10703-005-1491-3","type":"journal-article","created":{"date-parts":[[2005,8,25]],"date-time":"2005-08-25T10:33:31Z","timestamp":1124966011000},"page":"137-180","source":"Crossref","is-referenced-by-count":9,"title":["Translating Java for Multiple Model Checkers: The Bandera Back-End"],"prefix":"10.1007","volume":"26","author":[{"given":"Radu","family":"Iosif","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Matthew B.","family":"Dwyer","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"John","family":"Hatcliff","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"1491_CR1","doi-asserted-by":"crossref","unstructured":"R. Alur, R. Grosu, and M. McDougall, \u201cEfficient reachability analysis of hierarchical reactive machines,\u201d in Proceedings 12th International Conference on Computer Aided Verification, 2000.","DOI":"10.1007\/10722167_23"},{"key":"1491_CR2","unstructured":"E. Ashcroft and Z. Manna, \u201cFormalization of properties of parallel programs,\u201d Machine Intelligence, pp. 17\u201341, 1972."},{"issue":"4","key":"1491_CR3","doi-asserted-by":"crossref","first-page":"317","DOI":"10.1007\/s100090050038","volume":"2","author":"George S. Avrunin","year":"2000","unstructured":"George S. Avrunin, James C. Corbett, and Matthew B. Dwyer, \u201cBenchmarking finite-state verifiers,\u201d International Journal on Software Tools for Technology Transfer, Vol. 2, No. 4, pp. 317\u2013320, 2000.","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"1491_CR4","doi-asserted-by":"crossref","unstructured":"T. Ball and S. Rajamani, \u201cBebop: A symbolic model-checker for boolean programs,\u201d in K. Havelund, John Penix, and Willem Visser (Eds.), Proceedings of Seventh International SPIN Workshop, volume 1885 of Lecture Notes in Computer Science, Springer-Verlag, 2000, pp. 113\u2013130.","DOI":"10.1007\/10722468_7"},{"key":"1491_CR5","unstructured":"Saddek Bensalem, Vijay Ganesh, Yassine Lakhnech, Cesar Mu noz, Sam Owre, Harald Rue\u00df, John Rushby, Vlad Rusu, Hassen Sa\u00efdi, N. Shankar, Eli Singerman, and Ashish Tiwari, \u201cAn overview of SAL,\u201d in Proceedings of the Fifth Langley Formal Methods Workshop, June 2000."},{"issue":"4","key":"1491_CR6","doi-asserted-by":"crossref","first-page":"410","DOI":"10.1007\/s100090050046","volume":"2","author":"A. Cimatti","year":"2000","unstructured":"A. Cimatti, E. Clarke, F. Giunchiglia, and M. Roveri, \u201cNuSMV : A new symbolic model checker,\u201d International Journal on Software Tools for Technology Transfer, Vol. 2, No. 4, pp. 410\u2013425, 2000.","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"1491_CR7","doi-asserted-by":"crossref","unstructured":"A. Cimatti, E. M. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore, M. Roveri, R. Sebastiani, and A. Tacchella, \u201cNusmv 2: An opensource tool for symbolic model checking,\u201d in Proceeding of International Conference on Computer-Aided Verification (CAV), 2002.","DOI":"10.1007\/3-540-45657-0_29"},{"key":"1491_CR8","unstructured":"E.M. Clarke and E.A. Emerson, \u201cSynthesis of synchronization skeletons for branching time temporal logic,\u201d Lecture Notes in Computer Science, Vol. 131, 1981."},{"key":"1491_CR9","doi-asserted-by":"crossref","unstructured":"James C. Corbett, Matthew B. Dwyer, John Hatcliff, Shawn Laubach, Corina S. P\u0103s\u0103reanu, Robby, and Hongjun Zheng, \u201cBandera: Extracting finite-state models from Java source code,\u201d in Proceedings of the 22nd International Conference on Software Engineering, June 2000.","DOI":"10.1145\/337180.337234"},{"key":"1491_CR10","doi-asserted-by":"crossref","unstructured":"James C. Corbett, Matthew B. Dwyer, John Hatcliff, and Robby, \u201cBandera: A source-level interface for model checking Java programs,\u201d in Proceedings of the 22nd International Conference on Software Engineering, June 2000.","DOI":"10.1145\/337180.337625"},{"key":"1491_CR11","doi-asserted-by":"crossref","unstructured":"James C. Corbett, Matthew B. Dwyer, John Hatcliff, and Robby, \u201cExpressing checkable properties of dynamic systems: The bandera specification language,\u201d International Journal on Software Tools for Technology Transfer, Vol. 4, No. 1, 2002.","DOI":"10.1007\/s100090200075"},{"key":"1491_CR12","doi-asserted-by":"crossref","unstructured":"Jeffrey Dean, David Grove, and Craig Chambers, \u201cOptimization of object-oriented programs using static class hierarchy analysis,\u201d Lecture Notes in Computer Science, Vol. 952, 1995.","DOI":"10.1007\/3-540-49538-X_5"},{"issue":"7","key":"1491_CR13","doi-asserted-by":"crossref","first-page":"577","DOI":"10.1002\/(SICI)1097-024X(199906)29:7<577::AID-SPE246>3.0.CO;2-V","volume":"29","author":"C. Demartini","year":"1999","unstructured":"C. Demartini, R. Iosif, and R. Sisto, \u201cA deadlock detection tool for concurrent Java programs,\u201d Software - Practice and Experience, Vol. 29, No. 7, pp. 577\u2013603, 1999.","journal-title":"Software - Practice and Experience"},{"key":"1491_CR14","doi-asserted-by":"crossref","unstructured":"C. Demartini, R. Iosif, and R. Sisto, \u201cdSPIN: A dynamic extension of SPIN,\u201d in Theoretical and Applied Aspects of SPIN Model Checking (LNCS 1680), September 1999.","DOI":"10.1007\/3-540-48234-2_20"},{"key":"1491_CR15","doi-asserted-by":"crossref","unstructured":"Xianghua Deng, Matthew B. Dwyer, John Hatcliff, and Masaaki Mizuno, \u201cinvariant-based specification, synthesis, and verification of synchronization in concurrent programs,\u201d in Proceedings of the 24nd International Conference on Software Engineering, May 2002.","DOI":"10.1145\/581339.581394"},{"key":"1491_CR16","doi-asserted-by":"crossref","unstructured":"Matthew Dwyer, John Hatcliff, Roby Joehanes, Shawn Laubach, Corina Pasareanu, Robby, Willem Visser, and Hongjun Zheng, \u201cTool-supported program abstraction for finite-state verification,\u201d in Proceedings of the 23rd International Conference on Software Engineering, 2001, pp. 177\u2013187.","DOI":"10.1109\/ICSE.2001.919092"},{"key":"1491_CR17","doi-asserted-by":"crossref","unstructured":"Matthew B. Dwyer, John Hatcliff, Roby Joehanes, Shawn Laubach, Corina S. P\u0103s\u0103reanu, Robby, Willem Visser, and Hongjun Zheng, \u201cTool-supported program abstraction for finite-state verification,\u201d in Proceedings of the 23rd International Conference on Software Engineering, May 2001.","DOI":"10.1109\/ICSE.2001.919092"},{"key":"1491_CR18","doi-asserted-by":"crossref","unstructured":"M.B. Dwyer, G.S. Avrunin, and J.C. Corbett, \u201cPatterns in property specifications for finite-state verification,\u201d in Proceedings of the 21st International Conference on Software Engineering, May 1999.","DOI":"10.1145\/302405.302672"},{"key":"1491_CR19","doi-asserted-by":"crossref","unstructured":"Stefan Edelkamp, Alberto Lluch-Lafuente, and Stefan Leue, \u201cDirected model-checking with HSF-Spin,\u201d in Proceedings of the 8th International SPIN Workshop on Software Model Checking, Lecture Notes in Computer Science, 2001.","DOI":"10.1007\/3-540-45139-0_5"},{"key":"1491_CR20","doi-asserted-by":"crossref","unstructured":"R. Gerth, R. Kuiper, D. Peled, and W. Penczek, \u201cA partial order approach to branching time logic model checking,\u201d in Proceedings 3rd Israel Symposium on Theory on Computing and Systems, 1995, pp. 130\u2013139.","DOI":"10.1109\/ISTCS.1995.377038"},{"key":"1491_CR21","unstructured":"Carlo Ghezzi and Mehdi Jazayeri, \u201cProgramming Language Concepts 3rd edition,\u201d John Wiley and Sons, 1997."},{"issue":"3","key":"1491_CR22","doi-asserted-by":"crossref","first-page":"555","DOI":"10.1145\/233551.233556","volume":"43","author":"R.J. van Glabbeek","year":"1996","unstructured":"R.J. van Glabbeek and W.P. Weijland, \u201cBranching time and abstraction in bisimulation semantics,\u201d Journal of the ACM, Vol. 43, No. 3, pp. 555\u2013600, 1996.","journal-title":"Journal of the ACM"},{"key":"1491_CR23","doi-asserted-by":"crossref","unstructured":"Patrice Godefroid, \u201cPartial-order methods for the verification of concurrent systems,\u201d Lecture Notes in Computer Science, Vol. 1032, 1996.","DOI":"10.1007\/3-540-60761-7"},{"key":"1491_CR24","doi-asserted-by":"crossref","unstructured":"Patrice Godefroid, \u201cModel-checking for programming languages using VeriSoft,\u201d in Proceedings of the 24th ACM Symposium on Principles of Programming Languages (POPL\u201997), January 1997, pp. 174\u2013186,","DOI":"10.1145\/263699.263717"},{"key":"1491_CR25","doi-asserted-by":"crossref","unstructured":"John Hatcliff, James C. Corbett, Matthew B. Dwyer, Stefan Sokolowski, and Hongjun Zheng, \u201cA formal study of slicing for multi-threaded programs with JVM concurrency primitives,\u201d in Proceedings of the 6th International Static Analysis Symposium (SAS\u201999), September 1999.","DOI":"10.1007\/3-540-48294-6_1"},{"key":"1491_CR26","unstructured":"John Hatcliff, Matthew B. Dwyer, Corina S. P\u0103s\u0103reanu, and Robby, \u201cFoundations of the bandera abstraction tools,\u201d in The Essence of Computation, LNCS 1490, 2000."},{"key":"1491_CR27","doi-asserted-by":"crossref","unstructured":"John Hatcliff, Matthew B. Dwyer, and Hongjun Zheng, \u201cSlicing software for model construction,\u201d Higher-order and Symbolic Computation, Vol. 13, No. 4, 2000.","DOI":"10.1023\/A:1026599015809"},{"key":"1491_CR28","doi-asserted-by":"crossref","unstructured":"K. Havelund and T. Pressburger, \u201cModel checking Java programs using Java PathFinder,\u201d International Journal on Software Tools for Technology Transfer, 1999.","DOI":"10.1007\/s100090050043"},{"key":"1491_CR29","doi-asserted-by":"crossref","unstructured":"Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, and Gregoire Sutre, \u201cLazy abstraction,\u201d in Proceedings of the ACM SIGPLAN-SIGACT Conference on Principles of Programming Languages, Portland, Oregon, January 2002.","DOI":"10.1145\/503272.503279"},{"key":"1491_CR30","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"Gerard Holzmann","year":"1997","unstructured":"Gerard Holzmann, \u201cThe spin model checker,\u201d IEEE Transactions on Software Engineering, Vol. 23, pp. 279\u2013295, 1997.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"1491_CR31","doi-asserted-by":"crossref","unstructured":"Gerard Holzmann and Doron Peled, \u201cAn improvement in formal verification,\u201d Formal Description Techniques, pp. 197\u2013211, 1994.","DOI":"10.1007\/978-0-387-34878-0_13"},{"issue":"5","key":"1491_CR32","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"Gerard J. Holzmann","year":"1997","unstructured":"Gerard J. Holzmann, \u201cThe model checker SPIN,\u201d IEEE Transactions on Software Engineering, Vol. 23, No. 5, pp. 279\u2013294, 1997.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"1491_CR33","doi-asserted-by":"crossref","unstructured":"Gerard J. Holzmann and Margaret H. Smith, \u201cSoftware model checking: Extracting verification models from source code,\u201d in Proceedings of FORTE\/PSTV\u201999, November 1999.","DOI":"10.1007\/978-0-387-35578-8_28"},{"key":"1491_CR34","doi-asserted-by":"crossref","unstructured":"Radu Iosif, \u201cExploiting heap symmetries in explicit-state model checking of software,\u201d in Proc 16th IEEE International Conference on Automated Software Engineering, 2001, pp. 254\u2013261.","DOI":"10.1109\/ASE.2001.989811"},{"key":"1491_CR35","doi-asserted-by":"crossref","unstructured":"Radu Iosif and Riccardo Sisto, \u201cdspin: A dynamic extension of spin,\u201d in Proc. 6th SPIN Workshop, Lecture Notes in Computer Science, 1999, Vol. 1680, pp. 261\u2013276.","DOI":"10.1007\/3-540-48234-2_20"},{"key":"1491_CR36","doi-asserted-by":"crossref","unstructured":"Radu Iosif and Riccardo Sisto, \u201cUsing garbage collection in model checking,\u201d in Proc. 7th SPIN Workshop, Lecture Notes in Computer Science, 2000, Vol. 1885, pp. 20\u201333.","DOI":"10.1007\/10722468_2"},{"key":"1491_CR37","unstructured":"Roby Joehanes, \u201cIncorporating UML State Charts into Bandera,\u201d PhD thesis, Kansas State University, 2002, \u201c(Master of Science thesis)."},{"key":"1491_CR38","doi-asserted-by":"crossref","unstructured":"T. Lev-Ami and M. Sagiv, \u201cTVLA: A system for implementing static analyses,\u201d in Proceedings of the 7th International Static Analysis Symposium (SAS\u201900), 2000.","DOI":"10.1007\/978-3-540-45099-3_15"},{"key":"1491_CR39","doi-asserted-by":"crossref","unstructured":"Tim Lindholm and Frank Yellin, The Java Virtual Machine Specification, Sun Microsystems, Inc., 1997.","DOI":"10.1016\/S1353-4858(97)83033-4"},{"key":"1491_CR40","doi-asserted-by":"crossref","unstructured":"Alberto Lluch-Lafuente, Stefan Edelkamp, and Stefan Leue, \u201cPartial order reduction in directed model checking,\u201d in Proceedings of the 9th International SPIN Workshop on Software Model Checking, Lecture Notes in Computer Science, Vol. 2318, 2002.","DOI":"10.1007\/3-540-46017-9_10"},{"key":"1491_CR41","unstructured":"L. Mounier M. Bozga, and S. Graf, \u201cIF2.0: A validation environment for component-based real-time systems,\u201d in Proceedings of the Fourteenth International Conference on Computer-Aided Verification (CAV 2002) (LNCS 2404), July 2002."},{"key":"1491_CR42","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli, The Temporal Logic of Reactive and Concurrent Systems: Specification, Springer-Verlag, 1991.","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"1491_CR43","unstructured":"S.S. Muchnick, Advanced Compiler Design and Implementation, Morgan Kaufmann Publishers, 1997."},{"key":"1491_CR44","doi-asserted-by":"crossref","unstructured":"Rocco De Nicola and Frits Vaandrager, \u201cThree logics for branching bisimulation,\u201d in Proceedings of 5th Annual IEEE Symposium on Logic in Computer Science, 1990, pp. 118\u2013129.","DOI":"10.1109\/LICS.1990.113739"},{"key":"1491_CR45","doi-asserted-by":"crossref","unstructured":"S. Owre, J. M. Rushby, and N. Shankar, \u201cPVS: A prototype verification system,\u201d in Proceedings of the 1th International Conference on Automated Deduction (LNCS 607), 1992.","DOI":"10.1007\/3-540-55602-8_217"},{"key":"1491_CR46","doi-asserted-by":"crossref","unstructured":"Corina S. Pasareanu, Matthew B. Dwyer, and Willem Visser, \u201cFinding feasible counter-examples when model checking java programs,\u201d in Proceedings of Tools and Algorithms for the Construction and Analysis of Systems, 7th International Conference, Lecture Notes in Computer Science, Vol. 2031, 2001.","DOI":"10.1007\/3-540-45319-9_20"},{"key":"1491_CR47","doi-asserted-by":"crossref","unstructured":"Amir Pnueli, \u201cApplications of temporal logic to the specification and verification of reactive systems: A survey of current trends,\u201d Current Trends in Concurrency, Lecture Notes in Computer Science, pp. 510\u2013584, 1986.","DOI":"10.1007\/BFb0027047"},{"key":"1491_CR48","doi-asserted-by":"crossref","unstructured":"Corina S. P\u0103s\u0103reanu, Matthew B. Dwyer, and Willem Visser, \u201cFinding feasible counter-examples when model checking abstracted Java programs,\u201d in Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, volume 2031 of Lecture Notes in Computer Science. Springer-Verlag, April 2001.","DOI":"10.1007\/3-540-45319-9_20"},{"key":"1491_CR49","doi-asserted-by":"crossref","unstructured":"S. Stoller, \u201cModel-checking multi-threaded distributed Java programs,\u201d in K. Havelund, John Penix, and Willem Visser, (Eds.), Proceedings of Seventh International SPIN Workshop, volume 1885 of Lecture Notes in Computer Science, Springer-Verlag, 2000, pp. 224\u2013244.","DOI":"10.1007\/10722468_14"},{"key":"1491_CR50","unstructured":"Oksana Tkachuk, Adapting Side-effects Analysis for Java Environment Generation, PhD thesis, Kansas State University, 2003, \u201c(Master of Science thesis)."},{"key":"1491_CR51","doi-asserted-by":"crossref","unstructured":"Oksana Tkachuk and Matthew B. Dwyer, \u201cAdapting side effects analysis for modular program model checking,\u201d in Proceedings of the Fourth joint meeting of the European Software Engineering Conference and ACM SIGSOFT Symposium on the Foundations of Software Engineering, September 2003.","DOI":"10.1145\/940071.940097"},{"key":"1491_CR52","doi-asserted-by":"crossref","unstructured":"Oksana Tkachuk, Matthew B. Dwyer, and Corina S. P\u0103s\u0103reanu, \u201cAutomated environment generation for software model checking,\u201d in Proceedings of the Fourth joint meeting of the European Software Engineering Conference and ACM SIGSOFT Symposium on the Foundations of Software Engineering, October 2003.","DOI":"10.1109\/ASE.2003.1240300"},{"key":"1491_CR53","unstructured":"Raja Valle-Rai, Laurie Hendren, Vijay Sundaresan, Patrick Lam, Etienne Gagnon, and Phong Co, \u201cSoot - a Java optimization framework,\u201d in Proceedings of CASCON\u201999, November 1999."},{"key":"1491_CR54","doi-asserted-by":"crossref","unstructured":"W. Visser, G. Brat, K. Havelund, and S. Park, \u201cModel checking programs,\u201d in Proceedings of the 15th IEEE International Conference on Automated Software Engineering, September 2000.","DOI":"10.1109\/ASE.2000.873645"},{"key":"1491_CR55","doi-asserted-by":"crossref","unstructured":"Eran Yahav, \u201cVerifying safety properties of concurrent Java programs using 3-valued logic,\u201d in Proceedings of the ACM SIGPLAN-SIGACT Conference on Principles of Programming Languages, Jan 2001, pp. 27\u201340.","DOI":"10.1145\/360204.360206"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-005-1491-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-005-1491-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-005-1491-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,9]],"date-time":"2020-04-09T06:15:53Z","timestamp":1586412953000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-005-1491-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,3]]},"references-count":55,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2005,3]]}},"alternative-id":["1491"],"URL":"https:\/\/doi.org\/10.1007\/s10703-005-1491-3","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005,3]]}}}