{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T18:22:10Z","timestamp":1725560530757},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540213130"},{"type":"electronic","value":"9783540247258"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-24725-8_27","type":"book-chapter","created":{"date-parts":[[2010,7,27]],"date-time":"2010-07-27T20:15:44Z","timestamp":1280261744000},"page":"385-400","source":"Crossref","is-referenced-by-count":23,"title":["Extracting a Data Flow Analyser in Constructive Logic"],"prefix":"10.1007","author":[{"given":"David","family":"Cachera","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Jensen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Pichardie","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vlad","family":"Rusu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"27_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/3-540-45418-7_2","volume-title":"Smart Card Programming and Security","author":"G. Barthe","year":"2001","unstructured":"Barthe, G., Dufay, G., Huisman, M., de Sousa, S.M.: Jakarta: A Toolset for Reasoning about JavaCard. In: Attali, S., Jensen, T. (eds.) E-smart 2001. LNCS, vol.\u00a02140, p. 2. Springer, Heidelberg (2001)"},{"key":"27_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"302","DOI":"10.1007\/3-540-45309-1_20","volume-title":"Programming Languages and Systems","author":"G. Barthe","year":"2001","unstructured":"Barthe, G., Dufay, G., Jakubiec, L., Serpette, B.P., de Sousa, S.M.: A Formal Executable Semantics of the JavaCard Platform. In: Sands, D. (ed.) ESOP 2001. LNCS, vol.\u00a02028, p. 302. Springer, Heidelberg (2001)"},{"key":"27_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1007\/3-540-44585-4_3","volume-title":"Computer Aided Verification","author":"Y. Bertot","year":"2001","unstructured":"Bertot, Y.: Formalizing a JVML Verifier for Initialization in a Theorem Prover. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, p. 14. Springer, Heidelberg (2001)"},{"key":"27_CR4","doi-asserted-by":"crossref","unstructured":"Casset, L., Burdy, L., Requet, A.: Formal Development of an embedded verifier for Java Card Byte Code. In: Proc. of IEEE Int. Conference on Dependable Systems & Networks, DSN (2002)","DOI":"10.1109\/DSN.2002.1028886"},{"key":"27_CR5","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1145\/512950.512973","volume-title":"Proc. of 4th ACM Symposium on Principles of Programming Languages","author":"P. Cousot","year":"1977","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction of approximations of fixpoints. In: Proc. of 4th ACM Symposium on Principles of Programming Languages, pp. 238\u2013252. ACM Press, New York (1977)"},{"key":"27_CR6","unstructured":"Coglio, A., Goldberg, A., Qian, Z.: Towards a Provably-Correct Implementation of the JVM Bytecode Verifier. In: Proc. OOPSLA 1998 Workshop on Formal Underpinnings of Java (1998)"},{"key":"27_CR7","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1109\/ASE.2001.989789","volume-title":"Proc. of 16th Int. Conf. on Automated Software Engineering (ASE 2001)","author":"E. Denney","year":"2001","unstructured":"Denney, E.: The synthesis of a Java Card tokenisation algorithm. In: Proc. of 16th Int. Conf. on Automated Software Engineering (ASE 2001), pp. 43\u201350. IEEE Press, Los Alamitos (2001)"},{"key":"27_CR8","unstructured":"Genet, T., Jensen, T., Kodati, V., Pichardie, D.: A Java Card CAP converter in PVS. In: Proc. of 2nd International Workshop on Compiler Optimization Meets Compiler Verification, COCV 2003 (2003)"},{"key":"27_CR9","unstructured":"Hansen, R.R.: Flow Logic for Carmel. Technical Report SECSAFE-IMM-001, Danish Technical University (2002)"},{"issue":"3","key":"27_CR10","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1016\/S0304-3975(02)00869-1","volume":"298","author":"G. Klein","year":"2002","unstructured":"Klein, G., Nipkow, T.: Verified Bytecode Verifiers. Theoretical Computer Science\u00a0298(3), 583\u2013626 (2002)","journal-title":"Theoretical Computer Science"},{"key":"27_CR11","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1145\/781131.781156","volume-title":"Proc. of the ACM SIGPLAN 2003 conference on Programming language design and implementation","author":"S. Lerner","year":"2003","unstructured":"Lerner, S., Millstein, T., Chambers, C.: Automatically proving the correctness of compiler optimizations. In: Proc. of the ACM SIGPLAN 2003 conference on Programming language design and implementation, pp. 220\u2013231. ACM Press, New York (2003)"},{"key":"27_CR12","unstructured":"Marlet, R.: Syntax of the JCVM language to be studied in the SecSafe project. Technical Report SECSAFE-TL-005, Trusted Logic SA (May 2001)"},{"key":"27_CR13","unstructured":"Monniaux, D.: R\u00e9alisation m\u00e9canis\u00e9e d\u2019interpr\u00e9teurs abstraits. Rapport de DEA, Universit\u00e9 Paris VII (1998) (in French)"},{"key":"27_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/BFb0026426","volume-title":"Compiler Construction","author":"H.R. Nielson","year":"1998","unstructured":"Nielson, H.R., Nielson, F.: Flow Logics for Constraint Based Analysis. In: Koskimies, K. (ed.) CC 1998. LNCS, vol.\u00a01383, pp. 109\u2013127. Springer, Heidelberg (1998)"},{"key":"27_CR15","unstructured":"Okasaki, C., Gill, A.: Fast mergeable integer maps. In: Workshop on ML, pp. 77\u201386 (1998)"},{"key":"27_CR16","unstructured":"Prost, F.: Interpr\u00e9tation de l\u2019analyse statique en th\u00e9orie des types. PhD thesis, \u00c9cole normale sup\u00e9rieure de Lyon (1999) (in French)"},{"key":"27_CR17","doi-asserted-by":"crossref","unstructured":"Siveroni, I.: Operational semantics of the Java Card Virtual Machine. J. Logic and Automated Reasoning (2004) (to appear)","DOI":"10.1016\/j.jlap.2003.07.003"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-24725-8_27","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,17]],"date-time":"2019-03-17T08:26:57Z","timestamp":1552811217000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-24725-8_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540213130","9783540247258"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-24725-8_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}