{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:48:02Z","timestamp":1749124082217},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540434771"},{"type":"electronic","value":"9783540460176"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-46017-9_6","type":"book-chapter","created":{"date-parts":[[2010,3,29]],"date-time":"2010-03-29T21:12:13Z","timestamp":1269897133000},"page":"42-59","source":"Crossref","is-referenced-by-count":4,"title":["Bytecode Model Checking: An Experimental Analysis"],"prefix":"10.1007","author":[{"given":"David","family":"Basin","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stefan","family":"Friedrich","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marek","family":"Gawkowski","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joachim","family":"Posegga","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,5,23]]},"reference":[{"key":"6_CR1","series-title":"Lect Notes Comput Sci","volume-title":"TACAS\u201999","author":"A. Biere","year":"1999","unstructured":"A. Biere, A. Cimatti, E. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In TACAS\u201999, volume 1579 of LNCS, Amsterdam, the Netherlands, 1999. Springer-Verlag."},{"key":"6_CR2","unstructured":"R. Cohen. The defensive java virtual machine specification. Technical report, Computational Logic Inc., 1997."},{"issue":"6","key":"6_CR3","doi-asserted-by":"publisher","first-page":"1196","DOI":"10.1145\/330643.330646","volume":"21","author":"S. N. Freund","year":"1999","unstructured":"S. N. Freund and J. C. Mitchell. The type system for object initialization in the Java bytecode language. ACM Transactions on Programming Languages and Systems, 21(6):1196\u20131250, Nov. 1999.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"5","key":"6_CR4","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G. J. Holzmann","year":"1997","unstructured":"G. J. Holzmann. The Spin model checker. IEEE Transactions on Software Engineering, 23(5):279\u2013295, May 1997.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"6_CR5","unstructured":"K. McMillan. Symbolic Model Checking: An Approach to the State Explosion Problem. PhD thesis, School of Computer Science, Carnegie Mellon University, Pittsburgh, PA, May 1992. CMU-CS-92-131."},{"key":"6_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1007\/3-540-44585-4_26","volume-title":"Computer Aided Verification","author":"X. Leroy","year":"2001","unstructured":"X. Leroy. Java bytecode verification: An overview. In Computer Aided Verification, 13th International Conference, volume 2001 of LNCS, pages 265\u2013285, Paris, France, July 2001. Springer-Verlag."},{"key":"6_CR7","volume-title":"The Java Series","author":"T. Lindholm","year":"1997","unstructured":"T. Lindholm and F. Yellin. The Java Virtual Machine Specification. Number 1102 in The Java Series. Addison-Wesley, Reading, MA, USA, Jan. 1997."},{"key":"6_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/3-540-45315-6_23","volume-title":"Foundations of Software Science and Computation Structures (FOSSACS 2001)","author":"T. Nipkow","year":"2001","unstructured":"T. Nipkow. Verified bytecode verifiers. In Foundations of Software Science and Computation Structures (FOSSACS 2001), volume 2030 of LNCS, pages 347\u2013363. Springer-Verlag, 2001."},{"key":"6_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1007\/BFb0055863","volume-title":"Byte code verification for Java smart cards based on model checking","author":"J. Posegga","year":"1998","unstructured":"J. Posegga and H. Vogt. Byte code verification for Java smart cards based on model checking. In Proceedings of the Fifth ESORICS, volume 1485 of LNCS, pages 175\u2013190, Louvain-la-Neuve, Belgium, Sept. 1998. Springer-Verlag."},{"key":"6_CR10","unstructured":"C. Pusch. Formalizing the Java Virtual Machine in Isabelle\/HOL. Technical Report TUM-I9816, Institut f\u00fcr Informatik, Technische Universi\u00e4t M\u00fcnchen, 1998."},{"key":"6_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/3-540-49059-0_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201999)","author":"C. Pusch","year":"1999","unstructured":"C. Pusch. Proving the soundness of a Java bytecode verifier specification in Isabelle\/HOL. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201999), volume 1579 of LNCS, pages 89\u2013103, Amsterdam, the Netherlands, 1999. Springer-Verlag."},{"key":"6_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/3-540-48737-9_8","volume-title":"Formal Syntax and Semantics of Java","author":"Z. Qian","year":"1999","unstructured":"Z. Qian. A formal specification of Java virtual machine instructions for objects, methods and subroutines. In Formal Syntax and Semantics of Java, volume 1523 of LNCS, pages 271\u2013311. Springer-Verlag, 1999."},{"issue":"4","key":"6_CR13","doi-asserted-by":"publisher","first-page":"638","DOI":"10.1145\/363911.363915","volume":"22","author":"Z. Qian","year":"2000","unstructured":"Z. Qian. Standard fixpoint iteration for Java bytecode verification. ACM Transactions on Programming Languages and Systems, 22(4):638\u2013672, 2000.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"6_CR14","doi-asserted-by":"crossref","unstructured":"D. Schmidt. Data flow analysis is model checking of abstract interpretations. In Conference record of POPL\u2019 98, pages 38\u201348, San Diego, 1998. ACM Press.","DOI":"10.1145\/268946.268950"},{"key":"6_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"351","DOI":"10.1007\/3-540-49727-7_22","volume-title":"Program analysis as model checking of abstract interpretations","author":"D. Schmidt","year":"1998","unstructured":"D. Schmidt and B. Steffen. Program analysis as model checking of abstract interpretations. In Proceedings of Static Analysis Symposium (SAS\u201998), volume 1503 of LNCS, pages 351\u2013380, Pisa, Italy, September 1998. Springer-Verlag."},{"key":"6_CR16","unstructured":"R. F. St\u00e4rk and J. Schmid. Java bytecode verification is not possible. In Formal Methods and Tools for Computer Science, Eurocast. Universidad de Las Palmas de Gran Canaria, 2001. Extended Abstract."},{"issue":"1","key":"6_CR17","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1145\/314602.314606","volume":"21","author":"R. Stata","year":"1999","unstructured":"R. Stata and M. Abadi. A type system for Java bytecode subroutines. ACM Transactions on Programming Languages and Systems, 21(1):90\u2013137, Jan. 1999.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"6_CR18","doi-asserted-by":"crossref","unstructured":"F. Yellin. Low level security in Java. In World Wide Web Journal: The Fourth International WWW Conference Proceedings, pages 369\u2013380, Cambridge, MA, 1995. O\u2019Reilly.","DOI":"10.1145\/3592626.3592656"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-46017-9_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,25]],"date-time":"2024-03-25T11:18:40Z","timestamp":1711365520000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-46017-9_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540434771","9783540460176"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/3-540-46017-9_6","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}