{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T11:33:42Z","timestamp":1742384022289},"publisher-location":"Boston, MA","reference-count":22,"publisher":"Springer US","isbn-type":[{"type":"print","value":"9781402081460"},{"type":"electronic","value":"9781402081477"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/1-4020-8147-2_1","type":"book-chapter","created":{"date-parts":[[2006,2,20]],"date-time":"2006-02-20T11:57:38Z","timestamp":1140436658000},"page":"1-16","source":"Crossref","is-referenced-by-count":11,"title":["Enforcing High-Level Security Properties for Applets"],"prefix":"10.1007","author":[{"given":"Mariela","family":"Pavlova","sequence":"first","affiliation":[]},{"given":"Gilles","family":"Barthe","sequence":"additional","affiliation":[]},{"given":"Lilian","family":"Burdy","sequence":"additional","affiliation":[]},{"given":"Marieke","family":"Huisman","sequence":"additional","affiliation":[]},{"given":"Jean-Louis","family":"Lanet","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"1_CR1","doi-asserted-by":"crossref","unstructured":"D. Bartetzko, C. Fischer, M. M\u00f6ller, and H. Wehrheim. Jass-Java with Assertions. In K. Havelund and G. Ro\u015fu, editors, ENTCS, volume 55(2). Elsevier Publishing, 2001.","DOI":"10.1016\/S1571-0661(04)00247-6"},{"key":"1_CR2","doi-asserted-by":"crossref","unstructured":"J. van den Berg and B. Jacobs. The LOOP compiler for Java and JML. In T. Margaria and W. Yi, editors, Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2001), number 2031 in LNCS, pages 299\u2013312. Springer, 2001.","DOI":"10.1007\/3-540-45319-9_21"},{"issue":"4","key":"1_CR3","doi-asserted-by":"crossref","first-page":"369","DOI":"10.3233\/JCS-2002-10404","volume":"10","author":"P. Bieber","year":"2002","unstructured":"P. Bieber, J. Cazin, V. Wiels, G. Zanon, P. Girard, and J.-L. Lanet. Checking Secure Interactions of Smart Card Applets: Extended version. Journal of Computer Security, 10(4):369\u2013398, 2002.","journal-title":"Journal of Computer Security"},{"key":"1_CR4","unstructured":"G. Brat, K. Havelund, S. Park, and W. Visser. Java PathFinder-second generation of a Java model checker. In Workshop on Advances in Verification, 2000."},{"key":"1_CR5","unstructured":"C. Breunesse, N. Cata\u00f1o, M. Huisman, and B. Jacobs. Formal Methods for Smart Cards: an experience report. Technical Report NIII-R0316, NIII, University of Nijmegen, 2003. To appear in Science of Computer Programming."},{"key":"1_CR6","doi-asserted-by":"crossref","unstructured":"L. Burdy, Y. Cheon, D. Cok, M. Ernst, J. Kiniry, G.T. Leavens, K.R.M. Leino, and E. Poll. An overview of JML tools and applications. In T. Arts and W. Fokkink, editors, Formal Methods for Industrial Critical Systems (FMICS 03), volume 80 of ENTCS. Elsevier, 2003.","DOI":"10.1016\/S1571-0661(04)80810-7"},{"key":"1_CR7","doi-asserted-by":"crossref","unstructured":"L. Burdy, A. Requet, and J.-L. Lanet. Java Applet Correctness: a Developer-Oriented Approach. In Formal Methods (FME\u201903), number 2805 in LNCS, pages 422\u2013439. Springer, 2003.","DOI":"10.1007\/978-3-540-45236-2_24"},{"key":"1_CR8","doi-asserted-by":"crossref","unstructured":"T. Colcombet and P. Fradet. Enforcing trace properties by program transformation. In Proceedings of POPL\u201900, pages 54\u201366. ACM Press, 2000.","DOI":"10.1145\/325694.325703"},{"key":"1_CR9","doi-asserted-by":"crossref","unstructured":"M. Dwyer, G. Avrunin, and J. Corbett. Property Specification Patterns for Finite-state Verification. In 2nd Workshop on Formal Methods in Software Practice, pages 7\u201315, 1998.","DOI":"10.1145\/298595.298598"},{"key":"1_CR10","unstructured":"U. Erlingsson. The Inlined Reference Monitor Approach to Security Policy Enforcement. PhD thesis, Department of Computer Science, Cornell University, 2003. Available as Technical Report 2003-1916."},{"issue":"2","key":"1_CR11","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1109\/32.908957","volume":"27","author":"M.D. Ernst","year":"2001","unstructured":"M.D. Ernst, J. Cockrell, W.G. Griswold, and D. Notkin. Dynamically discovering likely program invariants to support program evolution. IEEE Transactions on Software Engineering, 27(2):1\u201325, 2001.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"1_CR12","doi-asserted-by":"crossref","unstructured":"C. Flanagan and K.R.M. Leino. Houdini, an annotation assistant for ESC\/Java. In J.N. Oliveira and P. Zave, editors, Formal Methods Europe 2001 (FME\u201901): Formal Methods for Increasing Software Productivity, number 2021 in LNCS, pages 500\u2013517. Springer, 2001.","DOI":"10.1007\/3-540-45251-6_29"},{"key":"1_CR13","unstructured":"K. Hamlen, G. Morrisett, and F.B. Schneider. Computability classes for enforcement mechanisms. Technical Report 2003-1908, Department of Computer Science, Cornell University, 2003."},{"key":"1_CR14","unstructured":"K.R.M. Leino, G. Nelson, and J.B. Saxe. ESC\/Java user\u2019s manual. Technical Report SRC 2000-002, Compaq System Research Center, 2000."},{"issue":"1\u20132","key":"1_CR15","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1016\/j.jlap.2003.07.006","volume":"58","author":"C. March\u00e9","year":"2004","unstructured":"C. March\u00e9, C. Paulin-Mohring, and X. Urbain. The Krakatoa tool for JML\/Java program certification. Journal of Logic and Algebraic Programming, 58(1\u20132): 89\u2013106, 2004.","journal-title":"Journal of Logic and Algebraic Programming"},{"key":"1_CR16","unstructured":"R. Marlet and D. Le M\u00e9tayer. Security properties and Java Card specificities to be studied in the SecSafe project, 2001. Number: SECSAFE-TL-006."},{"key":"1_CR17","doi-asserted-by":"crossref","unstructured":"J. Meyer and A. Poetzsch-Heffter. An architecture of interactive program provers. In S. Graf and M. Schwartzbach, editors, Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2000), number 1785 in LNCS, pages 63\u201377. Springer, 2000.","DOI":"10.1007\/3-540-46419-0_6"},{"key":"1_CR18","doi-asserted-by":"crossref","unstructured":"G.C. Necula. Proof-Carrying Code. In Proceedings of POPL\u201997, pages 106\u2013119. ACM Press, 1997.","DOI":"10.1145\/263699.263712"},{"key":"1_CR19","unstructured":"F.B. Schneider. Enforceable security policies. Technical Report TR99-1759, Cornell University, October 1999."},{"key":"1_CR20","doi-asserted-by":"crossref","unstructured":"L. Tan, J. Kim, and I. Lee. Testing and monitoring model-based generated program. In Proceeding of RV\u201903, volume 89 of ENTCS. Elsevier, 2003.","DOI":"10.1016\/S1571-0661(04)81046-6"},{"key":"1_CR21","doi-asserted-by":"crossref","unstructured":"K. Trentelman and M. Huisman. Extending JML Specifications with Temporal Logic. In H. Kirchner and C. Ringeissen, editors, Algebraic Methodology And Software Technology (AMAST\u201902), number 2422 in LNCS, pages 334\u2013348. Springer, 2002.","DOI":"10.1007\/3-540-45719-4_23"},{"key":"1_CR22","doi-asserted-by":"crossref","unstructured":"D. Walker. A Type System for Expressive Security Policies. In Proceedings of POPL\u2019 00, pages 254\u2013267. ACM Press, 2000.","DOI":"10.1145\/325694.325728"}],"container-title":["IFIP International Federation for Information Processing","Smart Card Research and Advanced Applications VI"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/1-4020-8147-2_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,16]],"date-time":"2019-04-16T21:04:25Z","timestamp":1555448665000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/1-4020-8147-2_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9781402081460","9781402081477"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/1-4020-8147-2_1","relation":{},"ISSN":["1571-5736"],"issn-type":[{"type":"print","value":"1571-5736"}],"subject":[],"published":{"date-parts":[[2004]]}}}