{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T20:27:26Z","timestamp":1725481646804},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540402541"},{"type":"electronic","value":"9783540448815"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-44881-0_24","type":"book-chapter","created":{"date-parts":[[2007,3,5]],"date-time":"2007-03-05T16:39:56Z","timestamp":1173112796000},"page":"337-351","source":"Crossref","is-referenced-by-count":10,"title":["Validation of the JavaCard Platform with Implicit Induction Techniques"],"prefix":"10.1007","author":[{"given":"Gilles","family":"Barthe","sequence":"first","affiliation":[]},{"given":"Sorin","family":"Stratulat","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,6,18]]},"reference":[{"key":"24_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1007\/3-540-45719-4_4","volume-title":"Proceedings of AMAST\u201902","author":"G. Barthe","year":"2002","unstructured":"G. Barthe, P. Courtieu, G. Dufay, and S. Melo de Sousa. Tool-Assisted Specification and Verification of the JavaCard Platform. In H. Kirchner and C. Ringessein, editors, Proceedings of AMAST\u201902, volume 2422 of Lecture Notes in Computer Science, pages 41\u201359. Springer-Verlag, 2002."},{"key":"24_CR2","unstructured":"G. Barthe and G. Dufay. Verified ByteCode Verifiers Revisited. Manuscript, 2003."},{"key":"24_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1007\/3-540-45418-7_2","volume-title":"Proceedings of e-SMART\u201901","author":"G. Barthe","year":"2001","unstructured":"G. Barthe, G. Dufay, M. Huisman, and S. Melo de Sousa. Jakarta: a toolset to reason about the JavaCard platform. In I. Attali and T. Jensen, editors, Proceedings of e-SMART\u201901, volume 2140 of Lecture Notes in Computer Science, pages 2\u201318. Springer-Verlag, 2001."},{"key":"24_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"32","DOI":"10.1007\/3-540-47813-2_3","volume-title":"Proceedings of VMCAI\u201902","author":"G. Barthe","year":"2002","unstructured":"G. Barthe, G. Dufay, L. Jakubiec, and S. Melo de Sousa. A formal correspondence between offensive and defensive JavaCard virtual machines. In A. Cortesi, editor, Proceedings of VMCAI\u201902, volume 2294 of Lecture Notes in Computer Science, pages 32\u201345. Springer-Verlag, 2002."},{"key":"24_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"302","DOI":"10.1007\/3-540-45309-1_20","volume-title":"Proceedings of ESOP\u201901","author":"G. Barthe","year":"2001","unstructured":"G. Barthe, G. Dufay, L. Jakubiec, B. Serpette, and S. Melo de Sousa. A Formal Executable Semantics of the JavaCard Platform. In D. Sands, editor, Proceedings of ESOP\u201901, volume 2028 of Lecture Notes in Computer Science, pages 302\u2013319. Springer-Verlag, 2001."},{"issue":"170","key":"24_CR6","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1016\/S0304-3975(96)80708-0","volume":"1\u20132","author":"A. Bouhoula","year":"1996","unstructured":"A. Bouhoula. Using induction and rewriting to verify and complete parameterized specifications. Theoretical Computer Science, 1\u20132(170):245\u2013276, 1996.","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"24_CR7","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1006\/jsco.1996.0076","volume":"23","author":"A. Bouhoula","year":"1997","unstructured":"A. Bouhoula. Automated theorem proving by test set induction. Journal of Symbolic Computation, 23(1):47\u201377, January 1997.","journal-title":"Journal of Symbolic Computation"},{"key":"24_CR8","unstructured":"R. S. Boyer and J S. Moore. Integrating decision procedures into heuristic theorem provers: A case study with linear arithmetic. ICSCA-CMP-44, University of Texas at Austin, 1985. Also published in Machine Intelligence 11, Oxford University Press, 1988."},{"key":"24_CR9","unstructured":"L. Casset, L. Burdy, and A. Requet. Formal Development of an Embedded Verifier for JavaCard ByteCode. In Proceedings of DSN\u201902. IEEE Computer Society, 2002."},{"key":"24_CR10","doi-asserted-by":"crossref","unstructured":"I. Cervesato, N. A. Durgin, P. D. Lincoln, J. C. Mitchell, and A. Scedrov. A meta-notation for protocol analysis. In 12th IEEE Computer Security Foundations Workshop. IEEE Computer Society Press, June 1999.","DOI":"10.1109\/CSFW.1999.779762"},{"key":"24_CR11","unstructured":"A. Coglio, A. Goldberg, and Z. Qian. Towards a Provably-Correct Implementation of the JVM Bytecode Verifier. In Formal Underpinnings of Java Workshop at OOPSLA, 1998."},{"key":"24_CR12","unstructured":"Coq Development Team. The Coq Proof Assistant User\u2019s Guide. Version 7.4, February 2003."},{"key":"24_CR13","unstructured":"G. Denker, J. Meseguer, and C. Talcott. Formal specification and analysis of active networks and communication protocols: The maude experience. In DARPA Information Survivability Conference and Exposition (DISCEX 2000). IEEE, 2000."},{"issue":"4","key":"24_CR14","doi-asserted-by":"publisher","first-page":"517","DOI":"10.1145\/503112.503115","volume":"33","author":"P. Hartel","year":"2001","unstructured":"P. Hartel and L. Moreau. Formalizing the Safety of Java, the Java Virtual Machine and Java Card. ACM Computing Surveys, 33(4):517\u2013558, December 2001.","journal-title":"ACM Computing Surveys"},{"key":"24_CR15","doi-asserted-by":"crossref","unstructured":"G. Klein. Verified Java Bytecode Verification. PhD thesis, Technical University Munich, 2003.","DOI":"10.1016\/S0304-3975(02)00869-1"},{"key":"24_CR16","doi-asserted-by":"crossref","unstructured":"G. Klein and T. Nipkow. Verified bytecode verifiers. Theoretical Computer Science, 2003. To appear.","DOI":"10.1016\/S0304-3975(02)00869-1"},{"issue":"3\u20134","key":"24_CR17","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1023\/A:1021975117537","volume":"29","author":"Q.-H. Nguyen","year":"2002","unstructured":"Q.-H. Nguyen, C. Kirchner, and H. Kirchner. External rewriting for skeptical proof assistants. Journal of Automated Reasoning, 29(3\u20134):309\u2013336, 2002.","journal-title":"Journal of Automated Reasoning"},{"key":"24_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"347","DOI":"10.1007\/3-540-45315-6_23","volume-title":"Proceedings of FOSSACS\u201901","author":"T. Nipkow","year":"2001","unstructured":"T. Nipkow. Verified Bytecode Verifiers. In F. Honsell and M. Miculan, editors, Proceedings of FOSSACS\u201901, volume 2030 of Lecture Notes in Computer Science, pages 347\u2013363. Springer-Verlag, 2001."},{"key":"24_CR19","doi-asserted-by":"crossref","unstructured":"R. St\u00e4rk, J. Schmid, and E. B\u00f6rger. Java and the Java Virtual Machine-Definition, Verification, Validation. Springer-Verlag, 2001.","DOI":"10.1007\/978-3-642-59495-3"},{"issue":"4","key":"24_CR20","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1006\/jsco.2000.0469","volume":"32","author":"S. Stratulat","year":"2001","unstructured":"S. Stratulat. A general framework to build contextual cover set induction provers. Journal of Symbolic Computation, 32(4):403\u2013445, September 2001.","journal-title":"Journal of Symbolic Computation"},{"key":"24_CR21","unstructured":"S. Stratulat. New uses of existential variables in implicit induction. In preparation."},{"key":"24_CR22","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"418","DOI":"10.1007\/3-540-36078-6_28","volume-title":"Proceedings of LPAR\u201902","author":"D. Syme","year":"2002","unstructured":"D. Syme and A. D. Gordon. Automating type soundness proofs via decision procedures and guided reductions. In M. Baaz and A. Voronkov, editors, Proceedings of LPAR\u201902, volume 2514 of Lecture Notes in Computer Science, pages 418\u2013434, 2002."}],"container-title":["Lecture Notes in Computer Science","Rewriting Techniques and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44881-0_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,10]],"date-time":"2023-05-10T21:19:10Z","timestamp":1683753550000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44881-0_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540402541","9783540448815"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/3-540-44881-0_24","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2003]]}}}