{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T00:36:55Z","timestamp":1725842215421},"publisher-location":"Berlin, Heidelberg","reference-count":40,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540747918"},{"type":"electronic","value":"9783540747925"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2007]]},"DOI":"10.1007\/978-3-540-74792-5_7","type":"book-chapter","created":{"date-parts":[[2008,1,29]],"date-time":"2008-01-29T07:32:45Z","timestamp":1201591965000},"page":"152-174","source":"Crossref","is-referenced-by-count":13,"title":["JACK\u00a0\u2014\u00a0A Tool for Validation of Security and Behaviour of Java Applications"],"prefix":"10.1007","author":[{"given":"Gilles","family":"Barthe","sequence":"first","affiliation":[]},{"given":"Lilian","family":"Burdy","sequence":"additional","affiliation":[]},{"given":"Julien","family":"Charles","sequence":"additional","affiliation":[]},{"given":"Benjamin","family":"Gr\u00e9goire","sequence":"additional","affiliation":[]},{"given":"Marieke","family":"Huisman","sequence":"additional","affiliation":[]},{"given":"Jean-Louis","family":"Lanet","sequence":"additional","affiliation":[]},{"given":"Mariela","family":"Pavlova","sequence":"additional","affiliation":[]},{"given":"Antoine","family":"Requet","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"7_CR1","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511624162","volume-title":"The B Book, Assigning Programs to Meanings","author":"J.-R. Abrial","year":"1996","unstructured":"Abrial, J.-R.: The B Book, Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)"},{"key":"7_CR2","unstructured":"Alagi\u0107, S., Royer, M.: Next generation of virtual platforms. Article in odbms.org (October 2005), http:\/\/odbms.org\/about_contributors_alagic.html"},{"key":"7_CR3","series-title":"Lecture Notes in Computer Science","first-page":"151","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"M. Barnett","year":"2005","unstructured":"Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: An overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol.\u00a03362, pp. 151\u2013171. Springer, Heidelberg (2005)"},{"key":"7_CR4","volume-title":"ENTCS","author":"D. Bartetzko","year":"2001","unstructured":"Bartetzko, D., Fischer, C., M\u00f6ller, M., Wehrheim, H.: Jass \u2013 Java with Assertions. In: Havelund, K., Ro\u015fu, G. (eds.) ENTCS, vol.\u00a055(2), Elsevier Publishing, Amsterdam (2001)"},{"key":"7_CR5","first-page":"86","volume-title":"Software Engineering and Formal Methods","author":"G. Barthe","year":"2005","unstructured":"Barthe, G., Pavlova, M., Schneider, G.: Precise analysis of memory consumption using program logics. In: Software Engineering and Formal Methods, pp. 86\u201395. IEEE Press, Los Alamitos (2005)"},{"key":"7_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/11679219_9","volume-title":"Formal Aspects in Security and Trust","author":"G. Barthe","year":"2006","unstructured":"Barthe, G., Rezk, T., Saabas, A.: Proof obligations preserving compilation. In: Dimitrakos, T., Martinelli, F., Ryan, P.Y.A., Schneider, S. (eds.) FAST 2005. LNCS, vol.\u00a03866, pp. 112\u2013126. Springer, Heidelberg (2006)"},{"key":"7_CR7","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Verification of Object-Oriented Software: The KeY Approach","year":"2007","unstructured":"Beckert, B., H\u00e4hnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software: The KeY Approach. LNCS (LNAI), vol.\u00a04334. Springer, Heidelberg (2007)"},{"key":"7_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/3-540-45319-9_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J. Berg van den","year":"2001","unstructured":"van den Berg, J., Jacobs, B.: The LOOP compiler for Java and JML. In: Margaria, T., Yi, W. (eds.) ETAPS 2001 and TACAS 2001. LNCS, vol.\u00a02031, pp. 299\u2013312. Springer, Heidelberg (2001)"},{"issue":"4","key":"7_CR9","doi-asserted-by":"crossref","first-page":"369","DOI":"10.3233\/JCS-2002-10404","volume":"10","author":"P. Bieber","year":"2002","unstructured":"Bieber, P., Cazin, J., Girard, P., Lanet, J.-L., Wiels, V., Zanon, G.: Checking secure interactions of smart card applets. Journal of Computer Security\u00a010(4), 369\u2013398 (2002)","journal-title":"Journal of Computer Security"},{"issue":"1-3","key":"7_CR10","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1016\/j.scico.2004.05.011","volume":"55","author":"C. Breunesse","year":"2005","unstructured":"Breunesse, C., Cata\u00f1o, N., Huisman, M., Jacobs, B.: Formal methods for smart cards: an experience report. Science of Computer Programming\u00a055(1-3), 53\u201380 (2005)","journal-title":"Science of Computer Programming"},{"key":"7_CR11","series-title":"Electronic Notes in Theoretical Computer Science","first-page":"73","volume-title":"Workshop on Formal Methods for Industrial Critical Systems","author":"L. Burdy","year":"2003","unstructured":"Burdy, L., Cheon, Y., Cok, D., Ernst, M., Kiniry, J.R., Leavens, G.T., Leino, K.R.M., Poll, E.: An overview of JML tools and applications. In: Arts, T., Fokkink, W. (eds.) Workshop on Formal Methods for Industrial Critical Systems. Electronic Notes in Theoretical Computer Science, vol.\u00a080, pp. 73\u201389. Elsevier Science, Inc, Amsterdam (2003) Preprint University of Nijmegen (TR NIII-R0309)"},{"key":"7_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1007\/978-3-540-71289-3_18","volume-title":"Fundamental Approaches to Software Engineering (FASE 2007)","author":"L. Burdy","year":"2007","unstructured":"Burdy, L., Huisman, M., Pavlova, M.: Preliminary design of BML: A behavioral interface specification language for Java bytecode. In: Fundamental Approaches to Software Engineering (FASE 2007). LNCS, vol.\u00a04422, pp. 215\u2013229. Springer, Heidelberg (2007)"},{"key":"7_CR13","doi-asserted-by":"crossref","unstructured":"Burdy, L., Pavlova, M.: Java bytecode specification and verification. In: Symposium on Applied Computing, pp. 1835\u20131839. Association of Computing Machinery Press (2006)","DOI":"10.1145\/1141277.1141708"},{"key":"7_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"422","DOI":"10.1007\/978-3-540-45236-2_24","volume-title":"FME 2003: Formal Methods","author":"L. Burdy","year":"2003","unstructured":"Burdy, L., Requet, A., Lanet, J.-L.: Java applet correctness: A developer-oriented approach. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol.\u00a02805, pp. 422\u2013439. Springer, Heidelberg (2003)"},{"key":"7_CR15","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"A. Chander","year":"2005","unstructured":"Chander, A., Espinosa, D., Islam, N., Lee, P., Necula, G.: JVer: A Java Verifier. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, Springer, Heidelberg (2005)"},{"key":"7_CR16","unstructured":"Charles, J.: Adding native specifications to JML. In: Workshop on Formal Techniques for Java Programs (2006)"},{"key":"7_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"108","DOI":"10.1007\/978-3-540-30569-9_6","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"D. Cok","year":"2005","unstructured":"Cok, D., Kiniry, J.R.: ESC\/Java2: Uniting ESC\/Java and JML. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol.\u00a03362, pp. 108\u2013128. Springer, Heidelberg (2005)"},{"key":"7_CR18","first-page":"54","volume-title":"Principles of Programming Languages, POPL\u201900","author":"T. Colcombet","year":"2000","unstructured":"Colcombet, T., Fradet, P.: Enforcing trace properties by program transformation. In: Principles of Programming Languages, POPL\u201900, pp. 54\u201366. ACM Press, New York (2000)"},{"key":"7_CR19","unstructured":"Coq development team: The Coq proof assistant reference manual V8.0. Technical Report 255, INRIA, France (mars 2004), http:\/\/coq.inria.fr\/doc\/main.html"},{"key":"7_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1007\/11733447_24","volume-title":"Smart Card Research and Advanced Applications","author":"A. Courbot","year":"2006","unstructured":"Courbot, A., Pavlova, M., Grimaud, G., Vandewalle, J.J.: A low-footprint Java-to-native compilation scheme using formal methods. In: Domingo-Ferrer, J., Posegga, J., Schreckling, D. (eds.) CARDIS 2006. LNCS, vol.\u00a03928, pp. 329\u2013344. Springer, Heidelberg (2006)"},{"key":"7_CR21","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/3-540-44404-1_7","volume-title":"Logic for Programming and Automated Reasoning","author":"D. Delahaye","year":"2000","unstructured":"Delahaye, D.: A tactic language for the system Coq. In: Parigot, M., Voronkov, A. (eds.) LPAR 2000. LNCS (LNAI), vol.\u00a01955, pp. 85\u201395. Springer, Heidelberg (2000)"},{"issue":"3","key":"7_CR22","doi-asserted-by":"crossref","first-page":"365","DOI":"10.1145\/1066100.1066102","volume":"52","author":"D. Detlefs","year":"2005","unstructured":"Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. Journal of the Association of Computing Machinery\u00a052(3), 365\u2013473 (2005)","journal-title":"Journal of the Association of Computing Machinery"},{"issue":"8","key":"7_CR23","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/360933.360975","volume":"18","author":"E.W. Dijkstra","year":"1975","unstructured":"Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Communications of the ACM\u00a018(8), 453\u2013457 (1975)","journal-title":"Communications of the ACM"},{"key":"7_CR24","unstructured":"Erlingsson, U.: The Inlined Reference Monitor Approach to Security Policy Enforcement. PhD thesis, Department of Computer Science, Cornell University. Available as Technical Report 2003-1916 (2003)"},{"issue":"2","key":"7_CR25","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1109\/32.908957","volume":"27","author":"M.D. Ernst","year":"2001","unstructured":"Ernst, M.D., Cockrell, J., Griswold, W.G., Notkin, D.: Dynamically discovering likely program invariants to support program evolution. IEEE Transactions on Software Engineering\u00a027(2), 1\u201325 (2001)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"7_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"500","DOI":"10.1007\/3-540-45251-6_29","volume-title":"FME 2001: Formal Methods for Increasing Software Productivity","author":"C. Flanagan","year":"2001","unstructured":"Flanagan, C., Leino, K.R.M.: Houdini, an annotation assistant for ESC\/Java. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol.\u00a02021, pp. 500\u2013517. Springer, Heidelberg (2001)"},{"key":"7_CR27","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Saxe, J.B.: Avoiding exponential explosion: Generating compact verification conditions. In: Principles of Programming Languages, pp. 193\u2013205. New York, USA. Association of Computing Machinery Press (2001)","DOI":"10.1145\/373243.360220"},{"key":"7_CR28","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1016\/j.jlap.2003.07.005","volume":"58","author":"B. Jacobs","year":"2004","unstructured":"Jacobs, B.: Weakest precondition reasoning for Java programs with JML annotations. Journal of Logic and Algebraic Programming\u00a058, 61\u201388 (2004)","journal-title":"Journal of Logic and Algebraic Programming"},{"key":"7_CR29","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1127878.1127884","volume":"31","author":"G.T. Leavens","year":"2006","unstructured":"Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: A behavioral interface specification language for Java. ACM SIGSOFT Software Engineering Notes\u00a031, 1\u201338 (2006)","journal-title":"ACM SIGSOFT Software Engineering Notes"},{"key":"7_CR30","doi-asserted-by":"crossref","unstructured":"Leavens, G.T., Leino, K.R.M., M\u00fcller, P.: Specification and verification challenges for sequential object-oriented programs. Formal Aspects of Computing (to appear, 2007)","DOI":"10.1007\/s00165-007-0026-7"},{"key":"7_CR31","unstructured":"Leavens, G.T., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D., Kiniry, J.: JML Reference Manual. In: Progress. Department of Computer Science, Iowa State University (July 2005), Available from http:\/\/www.jmlspecs.org"},{"key":"7_CR32","unstructured":"Lindholm, T., Yellin, F.: The JavaTM Virtual Machine Specification, 2nd edn. Sun Microsystems, Inc. (1999), http:\/\/java.sun.com\/docs\/books\/vmspec\/"},{"key":"7_CR33","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1016\/j.jlap.2003.07.006","volume":"58","author":"C. March\u00e9","year":"2004","unstructured":"March\u00e9, C., Paulin-Mohring, C., Urbain, X.: The Krakatoa tool for certification of Java\/JavaCard programs annotated with JML annotations. Journal of Logic and Algebraic Programming\u00a058, 89\u2013106 (2004)","journal-title":"Journal of Logic and Algebraic Programming"},{"key":"7_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1007\/3-540-46419-0_6","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J. Meyer","year":"2000","unstructured":"Meyer, J., Poetzsch-Heffter, A.: An architecture of interactive program provers. In: Graf, S., Schwartzbach, M. (eds.) ETAPS 2000 and TACAS 2000. LNCS, vol.\u00a01785, pp. 63\u201377. Springer, Heidelberg (2000)"},{"key":"7_CR35","doi-asserted-by":"crossref","unstructured":"Necula, G.C.: Proof-carrying code. In: Principles of Programming Languages, pp. 106\u2013119, New York, USA. Association of Computing Machinery Press (1997)","DOI":"10.1145\/263699.263712"},{"key":"7_CR36","unstructured":"Pavlova, M.: Specification and verification of Java bytecode. PhD thesis, Universit\u00e9 de Nice Sophia-Antipolis (2007)"},{"key":"7_CR37","volume-title":"CARDIS 2004","author":"M. Pavlova","year":"2004","unstructured":"Pavlova, M., Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L.: Enforcing high-level security properties for applets. In: Paradinas, P., Quisquater, J.-J. (eds.) CARDIS 2004, Kluwer Academic Publishing, Dordrecht (2004)"},{"key":"7_CR38","unstructured":"Schneider, F.B.: Enforceable security policies. Technical Report TR99-1759, Cornell University (October 1999)"},{"key":"7_CR39","unstructured":"The Coq Development Team: The Coq Proof Assistant Reference Manual \u2013 Version V8.1 (July 2006), http:\/\/coq.inria.fr"},{"key":"7_CR40","unstructured":"Winterstein, D., Aspinall, D., L\u00fcth, C.: Proof General\/Eclipse: A generic interface for interactive proof. In: International Workshop on User Interfaces for Theorem Provers 2005 (UITP\u201905) (2005)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Components and Objects"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-74792-5_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,7]],"date-time":"2019-05-07T08:57:18Z","timestamp":1557219438000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-74792-5_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007]]},"ISBN":["9783540747918","9783540747925"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-74792-5_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2007]]}}}