{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,12,29]],"date-time":"2022-12-29T06:50:36Z","timestamp":1672296636804},"reference-count":44,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2006,6,22]],"date-time":"2006-06-22T00:00:00Z","timestamp":1150934400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2006,10,18]]},"DOI":"10.1007\/s10817-005-0084-6","type":"journal-article","created":{"date-parts":[[2006,6,27]],"date-time":"2006-06-27T13:27:14Z","timestamp":1151414834000},"page":"295-354","source":"Crossref","is-referenced-by-count":3,"title":["Tool-Assisted Specification and Verification of Typed Low-Level Languages"],"prefix":"10.1007","volume":"35","author":[{"given":"Gilles","family":"Barthe","sequence":"first","affiliation":[]},{"given":"Pierre","family":"Courtieu","sequence":"additional","affiliation":[]},{"given":"Guillaume","family":"Dufay","sequence":"additional","affiliation":[]},{"given":"Sim\u00e3o","family":"Melo de Sousa","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2006,6,22]]},"reference":[{"key":"84_CR1","unstructured":"Alvarado, C. and Nguyen, Q.-H.: elan for equational reasoning in coq, in J. Despeyroux (ed.), Proceedings of LFM'00, Rapport Technique INRIA, 2000."},{"key":"84_CR2","unstructured":"Andronick, J., Chetali, B. and Ly, O.: Using Coq to verify Java Card applet isolation properties, in D. Basin and B. Wolff (eds.), Proceedings of TPHOLs'03, Lecture Notes in Comput. Sci. 2758, Springer-Verlag, 2003, pp. 335\u2013351."},{"key":"84_CR3","doi-asserted-by":"crossref","unstructured":"Baader, F. and Nipkow, T.: Term Rewriting and All That, Cambridge University Press, 1998.","DOI":"10.1017\/CBO9781139172752"},{"key":"84_CR4","unstructured":"Barthe, G. and Courtieu, P.: Efficient reasoning about executable specifications in Coq, in V. Carre\u00f1o, C. Mu\u00f1oz and S. Tahar (eds.), Proceedings of TPHOLs'02, Lecture Notes in Comput. Sci. 2410, Springer-Verlag, 2002, pp. 31\u201346."},{"key":"84_CR5","unstructured":"Barthe, G. and Dufay, G.: A tool-assisted framework for certified bytecode verification, in Proceedings of FASE'04, Lecture Notes in Comput. Sci. 2984, Springer-Verlag, 2004, pp. 99\u2013113."},{"key":"84_CR6","unstructured":"Barthe, G., Dufay, G., Jakubiec, L. and Melo de Sousa, S.: A formal correspondence between offensive and defensive javacard virtual machines, in A. Cortesi (ed.), Proceedings of VMCAI'02, Lecture Notes in Comput. Sci. 2294, Springer-Verlag, 2002, pp. 32\u201345."},{"key":"84_CR7","unstructured":"Barthe, G., Dufay, G., Jakubiec, L., Serpette, B. and Melo de Sousa, S.: A formal executable semantics of the JavaCard platform, in D. Sands (ed.), Proceedings of ESOP'01, Lecture Notes in Comput. Sci. 2028, Springer-Verlag, 2001, pp. 302\u2013319."},{"key":"84_CR8","doi-asserted-by":"crossref","unstructured":"Barthe, G. and Rezk, T.: Non-interference for a JVM-like language, in M. F\u00e4hndrich (ed.), Proceedings of TLDI'05, ACM Press, 2005. To appear.","DOI":"10.1145\/1040294.1040304"},{"key":"84_CR9","unstructured":"Barthe, G. and Stratulat, S.: Using implicit induction techniques for the validation of the JavaCard platform, in R. Nieuwenhuis (ed.), Proceedings of RTA'03, Lecture Notes in Comput. Sci. 2706, Springer-Verlag, 2003, pp. 337\u2013351."},{"key":"84_CR10","unstructured":"Betarte, G., Chetali, B., Gim\u00e9nez, E., Loiseaux, C. and Ly, O.: Formal modeling and verification of the Java Card security architecture: From static checkings to embedded applet execution, in Proceedings of ESMART'02, 2002."},{"key":"84_CR11","unstructured":"Bezem, M., Klop, J. W. and de Vrijer, R. (eds.): Term Rewriting Systems, Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, 2003."},{"key":"84_CR12","doi-asserted-by":"crossref","unstructured":"B\u00f6rger, E. and St\u00e4rk, R.: Abstract State Machines \u2013 A Method for High-Level System Design and Analysis, Springer-Verlag, 2003.","DOI":"10.1007\/978-3-642-18216-7_2"},{"key":"84_CR13","doi-asserted-by":"crossref","unstructured":"Borovansk\u00fd, P., Cirstea, H., Dubois, H., Kirchner, C., Kirchner, H., Moreau, P.-E., Ringeissen, C. and Vittek, M.: The Elan V3.4. Manual, 2000.","DOI":"10.1016\/S1571-0661(04)00032-5"},{"key":"84_CR14","doi-asserted-by":"crossref","unstructured":"Borras, P., Cl\u00e9ment, D., Despeyroux, Th., Incerpi, J., Kahn, G., Lang, B. and Pascual, V.: Centaur: The system, in Proceedings of the ACM SIGSOFT\/SIGPLAN Software Engineering Symposium on Practical Software Development Environments, ACM Press, 1988, pp. 14\u201324.","DOI":"10.1145\/64135.65005"},{"issue":"1","key":"84_CR15","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1006\/jsco.1996.0076","volume":"23","author":"A. Bouhoula","year":"1997","unstructured":"Bouhoula, A.: Automated theorem proving by test set induction, J. Symbolic Comput. 23(1) (January 1997), 47\u201377.","journal-title":"J. Symbolic Comput."},{"key":"84_CR16","doi-asserted-by":"crossref","unstructured":"Bundy, A.: The use of explicit plans to guide proofs, in Proceedings of CADE-9, Lecture Notes in Comput. Sci. 310, Springer-Verlag, 1988, pp. 111\u2013120.","DOI":"10.1007\/BFb0012826"},{"key":"84_CR17","unstructured":"Coq Development Team: The Coq Proof Assistant User's Guide. Version 8.0, January 2004."},{"key":"84_CR18","doi-asserted-by":"crossref","unstructured":"Cousot, P. and Cousot, R.: Abstract Interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints, in Proceedings of POPL'77, ACM Press, 1977, pp. 238\u2013252.","DOI":"10.1145\/512950.512973"},{"key":"84_CR19","unstructured":"Crary, K. and Morrisett, G.: Type structure for low-level programming languages, in J. Wiedermann, P. van Emde Boas and M. Nielsen (eds.), Proceedings of ICALP'99, Lecture Notes in Comput. Sci. 1644, 1999, pp. 40\u201354."},{"key":"84_CR20","unstructured":"Delahaye, D.: A tactic language for the system Coq, in M. Parigot and A. Voronkov (eds.), Proceedings of LPAR'00, Lecture Notes in Comput. Sci. 1955, Springer-Verlag, 2000, pp. 85\u201395."},{"key":"84_CR21","unstructured":"Filli\u00e2tre, J.-C.: Why: A multi-language multi-prover verification tool, Research Report 1366, LRI, Universit\u00e9 Paris Sud, March 2003."},{"issue":"6","key":"84_CR22","doi-asserted-by":"crossref","first-page":"1196","DOI":"10.1145\/330643.330646","volume":"21","author":"S. N. Freund","year":"1999","unstructured":"Freund, S. N. and Mitchell, J. C.: The type system for object initialization in the Java bytecode language, ACM Transactions on Programming Languages and Systems 21(6) (November 1999), 1196\u20131250.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"84_CR23","doi-asserted-by":"crossref","unstructured":"Gordon, A. D. and Syme, D.: Typing a multi-language intermediate code, in Proceedings of POPL'01, ACM Press, 2001, pp. 248\u2013260.","DOI":"10.1145\/360204.360228"},{"issue":"5","key":"84_CR24","doi-asserted-by":"crossref","first-page":"1379","DOI":"10.1002\/(SICI)1097-024X(19991225)29:15<1379::AID-SPE286>3.0.CO;2-V","volume":"29","author":"P. Hartel","year":"1999","unstructured":"Hartel, P.: LETOS \u2013 a lightweight execution tool for operational semantics, Software \u2013 Practice and Experience 29(5) (September 1999), 1379\u20131416.","journal-title":"Software \u2013 Practice and Experience"},{"issue":"4","key":"84_CR25","doi-asserted-by":"crossref","first-page":"517","DOI":"10.1145\/503112.503115","volume":"33","author":"P. Hartel","year":"2001","unstructured":"Hartel, P. and Moreau, L.: Formalizing the safety of Java, the Java virtual machine and Java Card, ACM Computing Surveys 33(4) (December 2001), 517\u2013558.","journal-title":"ACM Computing Surveys"},{"key":"84_CR26","unstructured":"JavaCard Technology: http:\/\/java.sun.com\/products\/javacard ."},{"issue":"3","key":"84_CR27","doi-asserted-by":"crossref","first-page":"583","DOI":"10.1016\/S0304-3975(02)00869-1","volume":"298","author":"G. Klein","year":"2002","unstructured":"Klein, G. and Nipkow, T.: Verified bytecode verifiers, Theoret. Comput. Sci. 298(3) (April 2002), 583\u2013626.","journal-title":"Theoret. Comput. Sci."},{"issue":"3\u20134","key":"84_CR28","doi-asserted-by":"crossref","first-page":"363","DOI":"10.1023\/A:1025095122199","volume":"30","author":"G. Klein","year":"2003","unstructured":"Klein, G. and Wildmoser, M.: Verified bytecode subroutines, J. Automated Reasoning 30(3\u20134) (December 2003), 363\u2013398.","journal-title":"J. Automated Reasoning"},{"key":"84_CR29","unstructured":"Lanet, J.-L. and Requet, A.: Formal proof of smart card applets correctness, in J.-J. Quisquater and B. Schneier (eds.), Proceedings of CARDIS'98, Lecture Notes in Comput. Sci. 1820, Springer-Verlag, 1998, pp. 85\u201397."},{"issue":"1","key":"84_CR30","doi-asserted-by":"crossref","first-page":"741","DOI":"10.1016\/S0304-3975(02)00330-4","volume":"290","author":"C. Laneve","year":"2002","unstructured":"Laneve, C.: A type system for JVM threads, Theoret. Comp. Sci. 290(1) (October 2002), 741\u2013778.","journal-title":"Theoret. Comp. Sci."},{"key":"84_CR31","unstructured":"Leroy, X., Java bytecode verification: An overview, in G. Berry, H. Comon and A. Finkel (eds.), Proceedings of CAV'01, Lecture Notes in Comput. Sci. 2102 Springer-Verlag, 2001, pp. 265\u2013285."},{"issue":"3\u20134","key":"84_CR32","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1023\/A:1025055424017","volume":"30","author":"X. Leroy","year":"2003","unstructured":"Leroy, X.: Java bytecode verification: Algorithms and formalizations, J. Automated Reasoning 30(3\u20134) (December 2003), 235\u2013269.","journal-title":"J. Automated Reasoning"},{"key":"84_CR33","unstructured":"Leroy, X., Doligez, D., Garrigue, J., R\u00e9my, D. and Vouillon, J.: The Objective Caml system, release 3.00, 2000."},{"key":"84_CR34","unstructured":"Moore, J. S., Krug, R., Liu, H. and Porter, G.: Formal models of Java at the JVM level. A survey from the ACL2 perspective, in S. Drossopoulou (ed.), Proceedings of Formal Techniques for Java Programs, 2001."},{"issue":"3\u20134","key":"84_CR35","doi-asserted-by":"crossref","first-page":"309","DOI":"10.1023\/A:1021975117537","volume":"29","author":"Q.-H. Nguyen","year":"2002","unstructured":"Nguyen, Q.-H., Kirchner, C. and Kirchner, H.: External rewriting for skeptical proof assistants, J. Automated Reasoning 29(3\u20134) (2002), 309\u2013336.","journal-title":"J. Automated Reasoning"},{"key":"84_CR36","doi-asserted-by":"crossref","unstructured":"Nielson, F., Nielson, H. R. and Hankin, C.: Principles of Program Analysis, Springer-Verlag, 1999.","DOI":"10.1007\/978-3-662-03811-6"},{"key":"84_CR37","unstructured":"Nipkow, T.: Verified bytecode verifiers, in F. Honsell and M. Miculan (eds.), Proceedings of FOSSACS'01, Lecture Notes in Comput. Sci. 2030, Springer-Verlag, 2001, pp. 347\u2013363."},{"key":"84_CR38","unstructured":"Petersson, M.: Compiling natural semantics, Ph.D. thesis, Link\u00f6ping University, 1995."},{"key":"84_CR39","unstructured":"Slind, K.: Reasoning about terminating functional programs, Ph.D. thesis, TU M\u00fcnich, 1999."},{"key":"84_CR40","doi-asserted-by":"crossref","unstructured":"St\u00e4rk, R., Schmid, J. and B\u00f6rger, E.: Java and the Java Virtual Machine \u2013 Definition, Verification, Validation, Springer-Verlag, 2001.","DOI":"10.1007\/978-3-642-59495-3"},{"issue":"1","key":"84_CR41","doi-asserted-by":"crossref","first-page":"90","DOI":"10.1145\/314602.314606","volume":"21","author":"R. Stata","year":"1999","unstructured":"Stata, R. and Abadi, M.: A type system for Java bytecode subroutines, ACM Transactions on Programming Languages and Systems 21(1) (January 1999), 90\u2013137.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"84_CR42","unstructured":"Syme, D. and Gordon, A. D.: Automating type soundness proofs via decision procedures and guided reductions, in M. Baaz and A. Voronkov (eds.), Proceedings of LPAR'02, Lecture Notes in Comput. Sci. 2514, Springer-Verlag, 2002, pp. 418\u2013434."},{"key":"84_CR43","unstructured":"Terrasse, D.: Vers un environnement d'aide au d\u00e9veloppement de preuves en s\u00e9mantique naturelle, Ph.D. thesis, Ecole Nationale des Ponts et Chauss\u00e9es, 1995."},{"key":"84_CR44","doi-asserted-by":"crossref","unstructured":"van Deursen, A., Heering, J. and Klint, P. (eds.), Language Prototyping: An Algebraic Specification Approach, AMAST Series in Computing, World Scientific, 1996.","DOI":"10.1142\/3163"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-005-0084-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-005-0084-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-005-0084-6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T01:21:45Z","timestamp":1559265705000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-005-0084-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,6,22]]},"references-count":44,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2006,10,18]]}},"alternative-id":["84"],"URL":"https:\/\/doi.org\/10.1007\/s10817-005-0084-6","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,6,22]]}}}