{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T11:33:32Z","timestamp":1743075212295,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540336891"},{"type":"electronic","value":"9783540336914"}],"license":[{"start":{"date-parts":[[2006,1,1]],"date-time":"2006-01-01T00:00:00Z","timestamp":1136073600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11741060_8","type":"book-chapter","created":{"date-parts":[[2006,4,27]],"date-time":"2006-04-27T09:42:07Z","timestamp":1146130927000},"page":"138-154","source":"Crossref","is-referenced-by-count":1,"title":["Modular Proof Principles for Parameterised Concretizations"],"prefix":"10.1007","author":[{"given":"David","family":"Pichardie","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"8_CR1","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":"8_CR2","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":"8_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1007\/978-3-540-24725-8_27","volume-title":"Programming Languages and Systems","author":"D. Cachera","year":"2004","unstructured":"Cachera, D., Jensen, T., Pichardie, D., Rusu, V.: Extracting a Data Flow Analyser in Constructive Logic. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol.\u00a02986, pp. 385\u2013400. Springer, Heidelberg (2004)"},{"key":"8_CR4","doi-asserted-by":"crossref","unstructured":"Cachera, D., Jensen, T., Pichardie, D., Rusu, V.: Extracting a Data Flow Analyser in Constructive Logic. Theoretical Computer Science\u00a0342(1), 56\u201378 (2005); Extended version of [3]","DOI":"10.1016\/j.tcs.2005.06.004"},{"key":"8_CR5","unstructured":"The Coq Proof Assistant, \n                  \n                    http:\/\/coq.inria.fr\/"},{"key":"8_CR6","doi-asserted-by":"crossref","unstructured":"Cortesi, A., Le Charlier, B., Van Hentenryck, P.: Combinations of abstract domains for logic programming. In: POPL, pp. 227\u2013239 (1994)","DOI":"10.1145\/174675.177880"},{"key":"8_CR7","series-title":"NATO ASI Series F","volume-title":"Calculational System Design","author":"P. Cousot","year":"1999","unstructured":"Cousot, P.: The calculational design of a generic abstract interpreter. In: Broy, M., Steinbr\u00fcggen, R. (eds.) Calculational System Design. NATO ASI Series F. IOS Press, Amsterdam (1999)"},{"issue":"4","key":"8_CR8","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1093\/logcom\/2.4.511","volume":"2","author":"P. Cousot","year":"1992","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation frameworks. Journal of Logic and Computation\u00a02(4), 511\u2013547 (1992)","journal-title":"Journal of Logic and Computation"},{"issue":"3","key":"8_CR9","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":"8_CR10","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":"8_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/3-540-45789-5_11","volume-title":"Static Analysis","author":"A. Min\u00e9","year":"2002","unstructured":"Min\u00e9, A.: A few graph-based relational numerical abstract domains. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol.\u00a02477, pp. 117\u2013132. Springer, Heidelberg (2002)"},{"key":"8_CR12","unstructured":"The Objective Caml language, \n                  \n                    http:\/\/caml.inria.fr\/"},{"key":"8_CR13","unstructured":"Pollet, I.: Towards a generic framework for the abstract interpretation of Java. PhD thesis, Universit\u00e9 catholique de Louvain, Belgium (2004)"},{"key":"8_CR14","doi-asserted-by":"crossref","unstructured":"Rountev, A., Milanova, A., Ryder, B.G.: Points-to analysis for Java using cnnoted constraints. In: OOPSLA, pp. 43\u201355 (2001)","DOI":"10.1145\/504311.504286"},{"key":"8_CR15","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","Construction and Analysis of Safe, Secure, and Interoperable Smart Devices"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11741060_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T13:26:36Z","timestamp":1558272396000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11741060_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540336891","9783540336914"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/11741060_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}