{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T19:44:49Z","timestamp":1725565489246},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642156397"},{"type":"electronic","value":"9783642156403"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"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":[[2010]]},"DOI":"10.1007\/978-3-642-15640-3_17","type":"book-chapter","created":{"date-parts":[[2010,9,15]],"date-time":"2010-09-15T04:11:29Z","timestamp":1284523889000},"page":"253-267","source":"Crossref","is-referenced-by-count":8,"title":["Certified Result Checking for Polyhedral Analysis of Bytecode Programs"],"prefix":"10.1007","author":[{"given":"Fr\u00e9d\u00e9ric","family":"Besson","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":"Tiphaine","family":"Turpin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"17_CR1","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1109\/LICS.1990.113737","volume-title":"Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science","author":"S.F. Allen","year":"1990","unstructured":"Allen, S.F., Constable, R.L., Howe, D.J., Aitken, W.E.: The semantics of reflected proof. In: Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science, pp. 95\u2013105. IEEE Computer Society, Los Alamitos (1990)"},{"key":"17_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-540-24721-0_7","volume-title":"Fundamental Approaches to Software Engineering","author":"G. Barthe","year":"2004","unstructured":"Barthe, G., Dufay, G.: A tool-assisted framework for certified bytecode verification. In: Wermelinger, M., Margaria-Steffen, T. (eds.) FASE 2004. LNCS, vol.\u00a02984, pp. 99\u2013113. Springer, Heidelberg (2004)"},{"key":"17_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1007\/978-3-540-74464-1_4","volume-title":"Types for Proofs and Programs","author":"F. Besson","year":"2006","unstructured":"Besson, F.: Fast reflexive arithmetic tactics: the linear case and beyond. In: Altenkirch, T., McBride, C. (eds.) TYPES 2006. LNCS, vol.\u00a04502, pp. 48\u201362. Springer, Heidelberg (2006)"},{"key":"17_CR4","unstructured":"Besson, F., Jensen, T., Pichardie, D., Turpin, T.: Result certification for relational program analysis. Research Report 6333, Inria (2007), \n                    \n                      http:\/\/hal.inria.fr\/inria-00166930\/"},{"key":"17_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/978-3-540-71316-6_19","volume-title":"Programming Languages and Systems","author":"F. Besson","year":"2007","unstructured":"Besson, F., Jensen, T., Turpin, T.: Small witnesses for abstract interpretation based proofs. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol.\u00a04421, pp. 268\u2013283. Springer, Heidelberg (2007)"},{"issue":"1","key":"17_CR6","doi-asserted-by":"publisher","first-page":"56","DOI":"10.1016\/j.tcs.2005.06.004","volume":"342","author":"D. Cachera","year":"2005","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)","journal-title":"Theoretical Computer Science"},{"issue":"2","key":"17_CR7","doi-asserted-by":"publisher","first-page":"228","DOI":"10.1016\/0041-5553(65)90045-5","volume":"5","author":"N.V. Chernikova","year":"1965","unstructured":"Chernikova, N.V.: Algorithm for finding a general formula for the non-negative solutions of a system of linear inequalities. U.S.S.R Comp.\u00a0Mathematics and Mathematical Physics\u00a05(2), 228\u2013233 (1965)","journal-title":"U.S.S.R Comp.\u00a0Mathematics and Mathematical Physics"},{"key":"17_CR8","first-page":"238","volume-title":"Proc. of 4th ACM Symp.\u00a0on 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 Symp.\u00a0on Principles of Programming Languages, pp. 238\u2013252. ACM Press, New York (1977)"},{"key":"17_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-540-31987-0_3","volume-title":"Programming Languages and Systems","author":"P. Cousot","year":"2005","unstructured":"Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: The Astr\u00e9e analyser. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol.\u00a03444, pp. 21\u201330. Springer, Heidelberg (2005)"},{"key":"17_CR10","first-page":"84","volume-title":"Proc. of 5th ACM Symp.\u00a0on Principles of Programming Languages (POPL 1978)","author":"P. Cousot","year":"1978","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Proc. of 5th ACM Symp.\u00a0on Principles of Programming Languages (POPL 1978), pp. 84\u201397. ACM Press, New York (1978)"},{"key":"17_CR11","first-page":"235","volume-title":"Proc. of the 7th ACM international conference on Functional programming (ICFP 2002)","author":"B. Gr\u00e9goire","year":"2002","unstructured":"Gr\u00e9goire, B., Leroy, X.: A compiled implementation of strong reduction. In: Proc. of the 7th ACM international conference on Functional programming (ICFP 2002), pp. 235\u2013246. ACM Press, New York (2002)"},{"key":"17_CR12","unstructured":"Jeannet, B., the Apron team: The Apron library (2007)"},{"issue":"3","key":"17_CR13","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":"17_CR14","first-page":"173","volume-title":"Proc. of 34th ACM Symp. on Principles of Programming Languages (POPL 2007)","author":"D.K. Lee","year":"2007","unstructured":"Lee, D.K., Crary, K., Harper, R.: Towards a mechanized metatheory of Standard ML. In: Proc. of 34th ACM Symp. on Principles of Programming Languages (POPL 2007), pp. 173\u2013184. ACM Press, New York (2007)"},{"key":"17_CR15","first-page":"42","volume-title":"Proc.\u00a0of the 33rd ACM Symp.\u00a0on Principles of Programming Languages","author":"X. Leroy","year":"2006","unstructured":"Leroy, X.: Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In: Proc.\u00a0of the 33rd ACM Symp.\u00a0on Principles of Programming Languages, pp. 42\u201354. ACM Press, New York (2006)"},{"key":"17_CR16","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/s10990-006-8609-1","volume":"19","author":"A. Min\u00e9","year":"2006","unstructured":"Min\u00e9, A.: The octagon abstract domain. Higher-Order and Symbolic Computation\u00a019, 31\u2013100 (2006)","journal-title":"Higher-Order and Symbolic Computation"},{"key":"17_CR17","first-page":"330","volume-title":"Proc.\u00a0of 31st ACM Symp.\u00a0on Principles of Programming Languages (POPL 2004)","author":"M. M\u00fcller-Olm","year":"2004","unstructured":"M\u00fcller-Olm, M., Seidl, H.: Precise interprocedural analysis through linear algebra. In: Proc.\u00a0of 31st ACM Symp.\u00a0on Principles of Programming Languages (POPL 2004), pp. 330\u2013341. ACM Press, New York (2004)"},{"key":"17_CR18","unstructured":"Pichardie, D.: Interpr\u00e9tation abstraite en logique intuitioniste: extraction d\u2019analyseurs Java certifi\u00e9s. PhD thesis, Universit\u00e9 de Rennes 1 (2005)"},{"key":"17_CR19","volume-title":"Theory of Linear and Integer Programming","author":"A. Schrijver","year":"1998","unstructured":"Schrijver, A.: Theory of Linear and Integer Programming. Wiley, Chichester (1998)"},{"issue":"6","key":"17_CR20","doi-asserted-by":"publisher","first-page":"826","DOI":"10.1145\/268999.269003","volume":"44","author":"H. Wasserman","year":"1997","unstructured":"Wasserman, H., Blum, M.: Software reliability via run-time result-checking. Journal of the ACM\u00a044(6), 826\u2013849 (1997)","journal-title":"Journal of the ACM"},{"key":"17_CR21","doi-asserted-by":"crossref","unstructured":"Wildmoser, M., Chaieb, A., Nipkow, T.: Bytecode analysis for proof carrying code. In: Proc.\u00a0of 1st Workshop on Bytecode Semantics, Verification and Transformation, ENTCS (2005)","DOI":"10.1016\/j.entcs.2005.02.040"},{"key":"17_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/978-3-540-31987-0_23","volume-title":"Programming Languages and Systems","author":"M. Wildmoser","year":"2005","unstructured":"Wildmoser, M., Nipkow, T.: Asserting bytecode safety. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol.\u00a03444, pp. 326\u2013341. Springer, Heidelberg (2005)"},{"key":"17_CR23","unstructured":"The Coq development of the work, \n                    \n                      http:\/\/www.irisa.fr\/celtique\/ext\/polycert\/"},{"key":"17_CR24","first-page":"375","volume-title":"Proc.\u00a0of 15th IEEE Symposium on Logic in Computer Science (LICS 2000)","author":"H. Xi","year":"2000","unstructured":"Xi, H.: Imperative Programming with Dependent Types. In: Proc.\u00a0of 15th IEEE Symposium on Logic in Computer Science (LICS 2000), pp. 375\u2013387. IEEE, Los Alamitos (2000)"},{"key":"17_CR25","unstructured":"Xi, H., Xia, S.: Towards Array Bound Check Elimination in Java Virtual Machine Language. In: Proc.\u00a0of CASCOON 1999, pp. 110\u2013125 (1999)"}],"container-title":["Lecture Notes in Computer Science","Trustworthly Global Computing"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-15640-3_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,20]],"date-time":"2019-03-20T13:38:32Z","timestamp":1553089112000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-15640-3_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642156397","9783642156403"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-15640-3_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}