{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,4]],"date-time":"2026-03-04T14:17:47Z","timestamp":1772633867076,"version":"3.50.1"},"reference-count":14,"publisher":"Elsevier BV","issue":"1","license":[{"start":{"date-parts":[[2007,7,1]],"date-time":"2007-07-01T00:00:00Z","timestamp":1183248000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":2220,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[2007,7]]},"DOI":"10.1016\/j.entcs.2007.02.059","type":"journal-article","created":{"date-parts":[[2007,8,1]],"date-time":"2007-08-01T08:57:45Z","timestamp":1185958665000},"page":"35-50","source":"Crossref","is-referenced-by-count":17,"title":["Formal Translation of Bytecode into BoogiePL"],"prefix":"10.1016","volume":"190","author":[{"given":"Hermann","family":"Lehner","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter","family":"M\u00fcller","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/j.entcs.2007.02.059_bib001","first-page":"255","article-title":"A program logic for bytecode","volume":"141","author":"Bannwart","year":"2005","journal-title":"ENTCS"},{"key":"10.1016\/j.entcs.2007.02.059_bib002","series-title":"Formal Methods for Components and Object","first-page":"364","article-title":"Boogie: A modular reusable verifier for object-oriented programs","volume":"volume 4111","author":"Barnett","year":"2006"},{"key":"10.1016\/j.entcs.2007.02.059_bib003","series-title":"Program Analysis For Software Tools and Engineering","first-page":"82","article-title":"Weakest-precondition of unstructured programs","author":"Barnett","year":"2005"},{"key":"10.1016\/j.entcs.2007.02.059_bib004","series-title":"Programming Languages and Systems, Third Asian Symposium","first-page":"364","article-title":"A Typed Compositional Logic for a Stack-Based Abstract Machine","volume":"volume 3780","author":"Benton","year":"2005"},{"issue":"1","key":"10.1016\/j.entcs.2007.02.059_bib005","first-page":"1","volume":"85","author":"Beringer","year":"2003","journal-title":"ENTCS"},{"key":"10.1016\/j.entcs.2007.02.059_bib006","unstructured":"Mobius Consortium. Deliverable 3.1: Bytecode specification language and program logic. Available online from http:\/\/mobius.inria.fr, 2006"},{"key":"10.1016\/j.entcs.2007.02.059_bib007","unstructured":"R. DeLine and K. R. M. Leino. BoogiePL: A typed procedural language for checking object-oriented programs. Technical Report MSR-TR-2005-70, Microsoft Research, 2005"},{"key":"10.1016\/j.entcs.2007.02.059_bib008","unstructured":"J.-C. Filli\u00e2tre. Why: a multi-language multi-prover verification tool. Research Report 1366, LRI, Universit\u00e9 Paris Sud, 2003"},{"key":"10.1016\/j.entcs.2007.02.059_bib009","series-title":"International Conference on Formal Engineering Methods","first-page":"15","article-title":"Multi-prover verification of C programs","volume":"volume 3308","author":"Filli\u00e2tre","year":"2004"},{"issue":"5","key":"10.1016\/j.entcs.2007.02.059_bib010","doi-asserted-by":"crossref","first-page":"234","DOI":"10.1145\/543552.512558","article-title":"Extended static checking for Java","volume":"37","author":"Flanagan","year":"2002","journal-title":"SIGPLAN Notices"},{"key":"10.1016\/j.entcs.2007.02.059_bib011","series-title":"Principles of programming languages","first-page":"193","article-title":"Avoiding exponential explosion: generating compact verification conditions","author":"Flanagan","year":"2001"},{"issue":"1\u20132","key":"10.1016\/j.entcs.2007.02.059_bib012","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1016\/j.jlap.2003.07.006","article-title":"The Krakatoa tool for certification of Java\/JavaCard programs annotated in JML","volume":"58","author":"March\u00e9","year":"2004","journal-title":"Journal of Logic and Algebraic Programming"},{"key":"10.1016\/j.entcs.2007.02.059_bib013","series-title":"Programming Concepts and Methods","article-title":"Logical foundations for typed object-oriented languages","author":"Poetzsch-Heffter","year":"1998"},{"key":"10.1016\/j.entcs.2007.02.059_bib014","unstructured":"A. Suzuki. Translating Java bytecode to BoogiePL. Master's thesis, ETH Zurich, 2006. www.sct.inf.ethz.ch\/projects\/student_docs\/Alex_Suzuki"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066107005270?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066107005270?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,1,5]],"date-time":"2019-01-05T10:56:35Z","timestamp":1546685795000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066107005270"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,7]]},"references-count":14,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2007,7]]}},"alternative-id":["S1571066107005270"],"URL":"https:\/\/doi.org\/10.1016\/j.entcs.2007.02.059","relation":{},"ISSN":["1571-0661"],"issn-type":[{"value":"1571-0661","type":"print"}],"subject":[],"published":{"date-parts":[[2007,7]]}}}