{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,10]],"date-time":"2025-04-10T04:26:25Z","timestamp":1744259185811,"version":"3.40.4"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642335570"},{"type":"electronic","value":"9783642335587"}],"license":[{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-33558-7_43","type":"book-chapter","created":{"date-parts":[[2012,10,3]],"date-time":"2012-10-03T02:32:47Z","timestamp":1349231567000},"page":"593-607","source":"Crossref","is-referenced-by-count":8,"title":["Refining Abstract Interpretation Based Value Analysis with Constraint Programming Techniques"],"prefix":"10.1007","author":[{"given":"Olivier","family":"Ponsini","sequence":"first","affiliation":[]},{"given":"Claude","family":"Michel","sequence":"additional","affiliation":[]},{"given":"Michel","family":"Rueher","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"43_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/978-3-642-14203-1_11","volume-title":"Automated Reasoning","author":"A. Ayad","year":"2010","unstructured":"Ayad, A., March\u00e9, C.: Multi-Prover Verification of Floating-Point Programs. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS, vol.\u00a06173, pp. 127\u2013141. Springer, Heidelberg (2010)"},{"issue":"6","key":"43_CR2","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1016\/j.ipl.2004.10.015","volume":"93","author":"M. Barnett","year":"2005","unstructured":"Barnett, M., Leino, K.R.M.: Weakest-precondition of unstructured programs. Information Processing Letters\u00a093(6), 281\u2013288 (2005)","journal-title":"Information Processing Letters"},{"key":"43_CR3","doi-asserted-by":"crossref","unstructured":"Boldo, S., Filli\u00e2tre, J.C.: Formal verification of floating-point programs. In: 18th IEEE Symposium on Computer Arithmetic, pp. 187\u2013194. IEEE (2007)","DOI":"10.1109\/ARITH.2007.20"},{"issue":"2","key":"43_CR4","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1002\/stvr.333","volume":"16","author":"B. Botella","year":"2006","unstructured":"Botella, B., Gotlieb, A., Michel, C.: Symbolic execution of floating-point computations. Software Testing, Verification and Reliability\u00a016(2), 97\u2013121 (2006)","journal-title":"Software Testing, Verification and Reliability"},{"key":"43_CR5","doi-asserted-by":"crossref","unstructured":"Brillout, A., Kroening, D., Wahl, T.: Mixed abstractions for floating-point arithmetic. In: 9th International Conference on Formal Methods in Computer-Aided Design, pp. 69\u201376. IEEE (2009)","DOI":"10.1109\/FMCAD.2009.5351141"},{"key":"43_CR6","doi-asserted-by":"crossref","unstructured":"Codognet, P., Fil\u00e9, G.: Computations, abstractions and constraints in logic programs. In: International Conference on Computer Languages (ICCL 1992), pp. 155\u2013164. IEEE (1992)","DOI":"10.1109\/ICCL.1992.185478"},{"issue":"2","key":"43_CR7","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1007\/s10601-009-9089-9","volume":"15","author":"H. Collavizza","year":"2010","unstructured":"Collavizza, H., Rueher, M., Hentenryck, P.V.: A constraint-programming framework for bounded program verification. Constraints Journal\u00a015(2), 238\u2013264 (2010)","journal-title":"Constraints Journal"},{"key":"43_CR8","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R., Feret, J., Min\u00e9, A., Mauborgne, L., Monniaux, D., Rival, X.: Varieties of static analyzers: A comparison with ASTR\u00c9E. In: 1st Joint IEEE\/IFIP Symposium on Theoretical Aspects of Software Engineering, pp. 3\u201320. IEEE (2007)","DOI":"10.1109\/TASE.2007.55"},{"key":"43_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/978-3-642-04570-7_6","volume-title":"Formal Methods for Industrial Critical Systems","author":"D. Delmas","year":"2009","unstructured":"Delmas, D., Goubault, E., Putot, S., Souyris, J., Tekkal, K., V\u00e9drine, F.: Towards an Industrial Use of FLUCTUAT on Safety-Critical Avionics Software. In: Alpuente, M., Cook, B., Joubert, C. (eds.) FMICS 2009. LNCS, vol.\u00a05825, pp. 53\u201369. Springer, Heidelberg (2009)"},{"key":"43_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1007\/978-3-540-74970-7_19","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2007","author":"T. Denmat","year":"2007","unstructured":"Denmat, T., Gotlieb, A., Ducass\u00e9, M.: An Abstract Interpretation Based Combinator for Modelling While Loops in Constraint Programming. In: Bessi\u00e8re, C. (ed.) CP 2007. LNCS, vol.\u00a04741, pp. 241\u2013255. Springer, Heidelberg (2007)"},{"issue":"2","key":"43_CR11","doi-asserted-by":"publisher","first-page":"242","DOI":"10.1109\/TC.2010.128","volume":"60","author":"F. Dinechin de","year":"2011","unstructured":"de Dinechin, F., Lauter, C.Q., Melquiond, G.: Certifying the floating-point implementation of an elementary function using Gappa. IEEE Transactions on Computers\u00a060(2), 242\u2013253 (2011)","journal-title":"IEEE Transactions on Computers"},{"key":"43_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1007\/978-3-642-28756-5_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"V. D\u2019Silva","year":"2012","unstructured":"D\u2019Silva, V., Haller, L., Kroening, D., Tautschnig, M.: Numeric Bounds Analysis with Conflict-Driven Learning. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol.\u00a07214, pp. 48\u201363. Springer, Heidelberg (2012)"},{"key":"43_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1007\/978-3-642-14295-6_22","volume-title":"Computer Aided Verification","author":"K. Ghorbal","year":"2010","unstructured":"Ghorbal, K., Goubault, E., Putot, S.: A Logical Product Approach to Zonotope Intersection. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 212\u2013226. Springer, Heidelberg (2010)"},{"issue":"1","key":"43_CR14","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1145\/103162.103163","volume":"23","author":"D. Goldberg","year":"1991","unstructured":"Goldberg, D.: What every computer scientist should know about floating point arithmetic. ACM Computing Surveys\u00a023(1), 5\u201348 (1991)","journal-title":"ACM Computing Surveys"},{"key":"43_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/11823230_3","volume-title":"Static Analysis","author":"E. Goubault","year":"2006","unstructured":"Goubault, E., Putot, S.: Static Analysis of Numerical Algorithms. In: Yi, K. (ed.) SAS 2006. LNCS, vol.\u00a04134, pp. 18\u201334. Springer, Heidelberg (2006)"},{"key":"43_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/978-3-642-18275-4_17","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"E. Goubault","year":"2011","unstructured":"Goubault, E., Putot, S.: Static Analysis of Finite Precision Computations. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol.\u00a06538, pp. 232\u2013247. Springer, Heidelberg (2011)"},{"issue":"1","key":"43_CR17","doi-asserted-by":"publisher","first-page":"138","DOI":"10.1145\/1132973.1132980","volume":"32","author":"L. Granvilliers","year":"2006","unstructured":"Granvilliers, L., Benhamou, F.: Algorithm 852: RealPaver: an interval solver using constraint satisfaction techniques. ACM Transactions on Mathematical Software\u00a032(1), 138\u2013156 (2006)","journal-title":"ACM Transactions on Mathematical Software"},{"key":"43_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/3-540-48256-3_9","volume-title":"Theorem Proving in Higher Order Logics","author":"J. Harrison","year":"1999","unstructured":"Harrison, J.: A Machine-Checked Theory of Floating Point Arithmetic. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Th\u00e9ry, L. (eds.) TPHOLs 1999. LNCS, vol.\u00a01690, pp. 113\u2013130. Springer, Heidelberg (1999)"},{"key":"43_CR19","unstructured":"Lhomme, O.: Consistency techniques for numeric CSPs. In: 13th International Joint Conference on Artificial Intelligence, pp. 232\u2013238 (1993)"},{"key":"43_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"360","DOI":"10.1007\/978-3-642-15396-9_30","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2010","author":"B. Marre","year":"2010","unstructured":"Marre, B., Michel, C.: Improving the Floating Point Addition and Subtraction Constraints. In: Cohen, D. (ed.) CP 2010. LNCS, vol.\u00a06308, pp. 360\u2013367. Springer, Heidelberg (2010)"},{"key":"43_CR21","unstructured":"Michel, C.: Exact projection functions for floating-point number constraints. In: 7th International Symposium on Artificial Intelligence and Mathematics (2002)"},{"key":"43_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"524","DOI":"10.1007\/3-540-45578-7_36","volume-title":"Principles and Practice of Constraint Programming - CP 2001","author":"C. Michel","year":"2001","unstructured":"Michel, C., Rueher, M., Lebbah, Y.: Solving Constraints over Floating-Point Numbers. In: Walsh, T. (ed.) CP 2001. LNCS, vol.\u00a02239, pp. 524\u2013538. Springer, Heidelberg (2001)"},{"key":"43_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"706","DOI":"10.1007\/978-3-642-23786-7_53","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2011","author":"M. Pelleau","year":"2011","unstructured":"Pelleau, M., Truchet, C., Benhamou, F.: Octagonal Domains for Continuous Constraints. In: Lee, J. (ed.) CP 2011. LNCS, vol.\u00a06876, pp. 706\u2013720. Springer, Heidelberg (2011)"},{"key":"43_CR24","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1017\/S096249291000005X","volume":"19","author":"S.M. Rump","year":"2010","unstructured":"Rump, S.M.: Verification methods: Rigorous results using floating-point arithmetic. Acta Numerica\u00a019, 287\u2013449 (2010)","journal-title":"Acta Numerica"}],"container-title":["Lecture Notes in Computer Science","Principles and Practice of Constraint Programming"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-33558-7_43","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T22:14:37Z","timestamp":1744236877000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-33558-7_43"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642335570","9783642335587"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-33558-7_43","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}