{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:37:49Z","timestamp":1725485869302},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540003267"},{"type":"electronic","value":"9783540363774"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-36377-7_9","type":"book-chapter","created":{"date-parts":[[2007,6,6]],"date-time":"2007-06-06T19:03:07Z","timestamp":1181156587000},"page":"172-203","source":"Crossref","is-referenced-by-count":9,"title":["Foundations of the Bandera Abstraction Tools"],"prefix":"10.1007","author":[{"given":"John","family":"Hatcliff","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Matthew B.","family":"Dwyer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Corina S.","family":"P\u0103s\u0103reanu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"family":"Robby","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,12,16]]},"reference":[{"key":"9_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1007\/10722468_7","volume-title":"Proceedings of Seventh International SPIN Workshop","author":"T. Ball","year":"2000","unstructured":"T. Ball and S. Rajamani. Bebop: a symbolic model-checker for boolean programs. In K. Havelund, editor, Proceedings of Seventh International SPIN Workshop, volume 1885 of Lecture Notes in Computer Science, pages 113\u2013130. Springer-Verlag, 2000."},{"key":"9_CR2","doi-asserted-by":"crossref","unstructured":"Saddek Bensalem, Yassine Lakhnech, and Sam Owre. Computing abstractions of infinite state systems compositionally and automatically. In Proc. 10th International Conference on Computer Aided Verification, June 1998.","DOI":"10.1007\/BFb0028755"},{"key":"9_CR3","unstructured":"G. Brat, K. Havelund, S. Park, and W. Visser. Java PathFinder \u2014 a second generation of a Java model-checker. In Proceedings of the Workshop on Advances in Verification, July 2000."},{"key":"9_CR4","doi-asserted-by":"crossref","unstructured":"James C. Corbett, Matthew B. Dwyer, John Hatcliff, Shawn Laubach, Corina S. P\u0103s\u0103reanu, Robby, and Hongjun Zheng. Bandera: Extracting finite-state models from Java source code. In Proceedings of the 22nd International Conference on Software Engineering, June 2000.","DOI":"10.1145\/337180.337234"},{"key":"9_CR5","unstructured":"James C. Corbett, Matthew B. Dwyer, John Hatcliff, and Robby. Expressing checkable properties of dynamic systems: The Bandera Specification Language. International Journal on Software Tools for Technology Transfer, 2002. To appear."},{"key":"9_CR6","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Conference Record of the Fourth Annual ACM Symposium on Principles of Programming Languages, pages 238\u2013252, 1977.","DOI":"10.1145\/512950.512973"},{"key":"9_CR7","unstructured":"G.J. Holzmann D. Dams, W. Hesse. Abstracting C with abC. In Proc. 14th International Conference on Computer Aided Verification, July 2002."},{"issue":"2","key":"9_CR8","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1145\/244795.244800","volume":"19","author":"D. Dams","year":"1997","unstructured":"Dennis Dams, Rob Gerth, and Orna Grumberg. Abstract interpretation of reactive systems. ACM Transactions on Programming Languages and Systems, 19(2):253\u2013291, March 1997.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"9_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48234-2_20","volume-title":"Theoretical and Applied Aspects of SPIN Model Checking","author":"C. Demartini","year":"1999","unstructured":"C. Demartini, R. Iosif, and R. Sisto. dSPIN: A dynamic extension of SPIN. In Theoretical and Applied Aspects of SPIN Model Checking (LNCS 1680), September 1999."},{"key":"9_CR10","unstructured":"Matthew B. Dwyer, John Hatcliff, Roby Joehanes, Shawn Laubach, Corina S. P\u0103s\u0103reanu, Robby, Willem Visser, and Hongjun Zheng. Tool-supported program abstraction for finite-state verification. In Proceedings of the 23rd International Conference on Software Engineering, May 2001."},{"key":"9_CR11","doi-asserted-by":"crossref","unstructured":"M.B. Dwyer, G.S. Avrunin, and J.C. Corbett. Patterns in property specifications for finite-state verification. In Proceedings of the 21st International Conference on Software Engineering, May 1999.","DOI":"10.1145\/302405.302672"},{"key":"9_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"254","DOI":"10.1007\/3-540-46017-9_24","volume-title":"Proceedings of Ninth International SPIN Workshop","author":"M. M. Gallardo","year":"2002","unstructured":"M. M. Gallardo, J. Mart\u00ednez, P. Merino, and E. Pimentel. SPIN: Extending SPIN with abstraction. In Proceedings of Ninth International SPIN Workshop, volume 2318 of Lecture Notes in Computer Science, pages 254\u2013258. Springer-Verlag, 2002."},{"key":"9_CR13","unstructured":"Carsten K. Gomard and Neil D. Jones. atCompiler generation by partial evaluation. In G. X. Ritter, editor, Information Processing\u2019 89. Proceedings of the IFIP 11th World Computer Congress, pages 1139\u20131144. IFIP, North-Holland, 1989."},{"key":"9_CR14","doi-asserted-by":"crossref","unstructured":"John Hatcliff. An introduction to partial evaluation using a simple flowchart language. In John Hatcliff, Peter Thiemann, and Torben Mogensen, editors, Proceedings of the 1998 DIKU International Summer School on Partial Evaluation, Tutorials in Computer Science, Copenhagen, Denmark, June 1998.","DOI":"10.1007\/3-540-47018-2_2"},{"key":"9_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1007\/10722468_8","volume-title":"Proceedings of Seventh International SPIN Workshop","author":"G. Holzmann","year":"2000","unstructured":"G. Holzmann. Logic verification of ANSI-C code with SPIN. In K. Havelund, editor, Proceedings of Seventh International SPIN Workshop, volume 1885 of Lecture Notes in Computer Science, pages 131\u2013147. Springer-Verlag, 2000."},{"issue":"5","key":"9_CR16","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G. J. Holzmann","year":"1997","unstructured":"Gerard J. Holzmann. The model checker SPIN. IEEE Transactions on Software Engineering, 23(5):279\u2013294, May 1997.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"9_CR17","unstructured":"M. Huth and M. Ryan. Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press, 1999."},{"key":"9_CR18","unstructured":"Radu Iosif, Matthew B. Dwyer, and John Hatcliff. Translating Java for multiple model checkers: the bandera back end. Technical Report 2002-1, SAnToS Laboratory Technical Report Series, Kansas State University, Department of Computing and Information Sciences, 2002."},{"key":"9_CR19","unstructured":"Neil D. Jones, Carsten K. Gomard, and Peter Sestoft. Partial Evaluation and Automatic Program Generation. Prentice-Hall International, 1993."},{"key":"9_CR20","series-title":"Lect Notes Comput Sci","volume-title":"The 23rd International Symposium on Mathematical Foundations of Computer Science","author":"Y. Kesten","year":"1998","unstructured":"Y. Kesten and A. Pnueli. Modularization and abstraction: The keys to formal verification. In L. Brim, J. Gruska, and J. Zlatuska, editors, The 23rd International Symposium on Mathematical Foundations of Computer Science, volume 1450 of Lecture Notes in Computer Science. Springer-Verlag, 1998."},{"key":"9_CR21","unstructured":"T. Lev-Ami and M. Sagiv. TVLA: A framework for Kleene-based static analysis. In Proceedings of the 7th International Static Analysis Symposium (SAS\u201900), 2000."},{"key":"9_CR22","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":"9_CR23","doi-asserted-by":"crossref","unstructured":"Flemming Nielson, Hanne Riis Nielson, and Chris Hankin. Principles of Program Analysis. Springer Verlag, 1999.","DOI":"10.1007\/978-3-662-03811-6"},{"key":"9_CR24","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of the 1th International Conference on Automated Deduction","author":"S. Owre","year":"1992","unstructured":"S. Owre, J. M. Rushby, and N. Shankar. PVS: A prototype verification system. In Proceedings of the 1th International Conference on Automated Deduction (LNCS 607), 1992."},{"key":"9_CR25","unstructured":"Corina S. P\u0103s\u0103reanu. Abstraction and Modular Reasoning for the Verification of Software. PhD thesis, Kansas State University, 2001."},{"key":"9_CR26","series-title":"Lect Notes Comput Sci","volume-title":"Theoretical and Applied Aspects of SPIN Model Checking","author":"C. S. P\u0103s\u0103reanu","year":"1999","unstructured":"Corina S. P\u0103s\u0103reanu, Matthew B. Dwyer, and Michael Huth. Assume-guarantee model checking of software: A comparative case study. In Theoretical and Applied Aspects of SPIN Model Checking (LNCS 16 80), September 1999."},{"key":"9_CR27","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems","author":"C. S. P\u0103s\u0103reanu","year":"2001","unstructured":"Corina S. P\u0103s\u0103reanu, Matthew B. Dwyer, and Willem Visser. Finding feasible counter-examples when model checking abstracted Java programs. 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, April 2001."},{"key":"9_CR28","unstructured":"Rupak Majumdar Thomas A. Henzinger, Ranjit Jhala and Gregoire Sutre. Lazy abstraction. In Proceedings of the 29th ACM Symposium on Principles of Programming Languages (POPL\u201902), 2002."},{"key":"9_CR29","unstructured":"Raja Valle-Rai, Laurie Hendren, Vijay Sundaresan, Patrick Lam, Etienne Gagnon, and Phong Co. Soot-a Java optimization framework. In Proceedings of CASCON\u201999, November 1999."},{"key":"9_CR30","doi-asserted-by":"crossref","unstructured":"Eran Yahav. Verifying safety properties of concurrent Java programs using 3-valued logic. In Proceedings of the 28th ACM Symposium on Principles of Programming Languages (POPL\u201901), pages 27\u201340, January 2001.","DOI":"10.1145\/360204.360206"}],"container-title":["Lecture Notes in Computer Science","The Essence of Computation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36377-7_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T15:36:59Z","timestamp":1556465819000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36377-7_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540003267","9783540363774"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/3-540-36377-7_9","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}