{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T11:18:05Z","timestamp":1742383085465},"reference-count":17,"publisher":"IEEE Comput. Soc","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1109\/dsn.2002.1028886","type":"proceedings-article","created":{"date-parts":[[2003,6,25]],"date-time":"2003-06-25T18:14:31Z","timestamp":1056564871000},"page":"51-56","source":"Crossref","is-referenced-by-count":8,"title":["Formal development of an embedded verifier for Java Card byte code"],"prefix":"10.1109","author":[{"given":"L.","family":"Casset","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"L.","family":"Burdy","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"A.","family":"Requet","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"17","doi-asserted-by":"publisher","DOI":"10.1023\/B:JARS.0000021015.15794.82"},{"key":"15","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-48737-9_8","article-title":"A formal specification of java virtual machine instructions for objects, methods and subroutines","author":"qian","year":"1999","journal-title":"Formal Syntax and Semantics of Java"},{"key":"16","doi-asserted-by":"publisher","DOI":"10.1109\/HASE.2000.895449"},{"key":"13","article-title":"?Java: Embedding a programming language in a theorem prover","author":"nipkow","year":"2000","journal-title":"Foundations of Secure Computation"},{"key":"14","article-title":"Proving the soundness of a java bytecode verifier in Isabelle\/HOL","author":"pusch","year":"0","journal-title":"OOPSLA98 Workshop Formal Underpinnings of Java 1998"},{"key":"11","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263712"},{"key":"12","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45315-6_23"},{"key":"3","article-title":"Formal implementation of a verification algorithm using the B method","author":"casset","year":"2001","journal-title":"AFADL '2001"},{"article-title":"A coq formalization of a type checker for object initialization in the java virtual machine","year":"2000","author":"bertot","key":"2"},{"key":"1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162"},{"journal-title":"Java Card 2 1 1","year":"2000","author":"microsystems","key":"10"},{"key":"7","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45418-7_13"},{"key":"6","doi-asserted-by":"publisher","DOI":"10.1002\/cpe.597"},{"key":"5","doi-asserted-by":"publisher","DOI":"10.1109\/DISCEX.2000.821537"},{"key":"4","article-title":"A formal specification of the java bytecode semantics using the B method","author":"casset","year":"0","journal-title":"1st ECOOP Workshop on Formal Techniques for Java Programs June 1999"},{"journal-title":"Connected Limited Device Configuration","year":"2000","author":"microsystems","key":"9"},{"journal-title":"The Java Virtual Machine Specification","year":"1996","author":"lindholm","key":"8"}],"event":{"name":"International Conference on Dependable Systems and Networks","acronym":"DSN-02","location":"Washington, DC, USA"},"container-title":["Proceedings International Conference on Dependable Systems and Networks"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/7991\/22107\/01028886.pdf?arnumber=1028886","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,15]],"date-time":"2017-06-15T18:42:04Z","timestamp":1497552124000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/1028886\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":17,"URL":"https:\/\/doi.org\/10.1109\/dsn.2002.1028886","relation":{},"subject":[]}}