{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T17:04:46Z","timestamp":1751648686339},"reference-count":28,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2014,5,22]],"date-time":"2014-05-22T00:00:00Z","timestamp":1400716800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Autom Softw Eng"],"published-print":{"date-parts":[[2016,6]]},"DOI":"10.1007\/s10515-014-0154-2","type":"journal-article","created":{"date-parts":[[2014,5,21]],"date-time":"2014-05-21T11:36:06Z","timestamp":1400672166000},"page":"191-217","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["Verifying floating-point programs with constraint programming and abstract interpretation techniques"],"prefix":"10.1007","volume":"23","author":[{"given":"Olivier","family":"Ponsini","sequence":"first","affiliation":[]},{"given":"Claude","family":"Michel","sequence":"additional","affiliation":[]},{"given":"Michel","family":"Rueher","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2014,5,22]]},"reference":[{"key":"154_CR1","doi-asserted-by":"crossref","unstructured":"Ayad, A., March\u00e9, C.: Multi-prover verification of floating-point programs. In: Proceedings of the IJCAR, LNCS, vol. 6173, pp. 127\u2013141. Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-14203-1_11"},{"issue":"6","key":"154_CR2","doi-asserted-by":"crossref","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. Inf. Process. Lett. 93(6), 281\u2013288 (2005)","journal-title":"Inf. Process. Lett."},{"key":"154_CR3","doi-asserted-by":"crossref","unstructured":"Boldo, S., Filli\u00e2tre, JC.: Formal verification of floating-point programs. In: Proceedings of the 18th IEEE Symposium on Computer Arithmetic, IEEE, pp. 187\u2013194. IEEE (2007)","DOI":"10.1109\/ARITH.2007.20"},{"issue":"2","key":"154_CR4","doi-asserted-by":"crossref","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. Softw. Testing Verif. Reliab. 16(2), 97\u2013121 (2006)","journal-title":"Softw. Testing Verif. Reliab."},{"key":"154_CR5","doi-asserted-by":"crossref","unstructured":"Brillout, A., Kroening, D., Wahl, T.: Mixed abstractions for floating-point arithmetic. In: Proceedings of the 9th International Conference on Formal Methods in Computer-Aided Design, IEEE, pp. 69\u201376. IEEE (2009)","DOI":"10.1109\/FMCAD.2009.5351141"},{"key":"154_CR6","doi-asserted-by":"crossref","unstructured":"Codognet, P., Fil\u00e9, G.: Computations, abstractions and constraints in logic programs. In: Proceedings of the International Conference on Computer Languages (ICCL\u201992), IEEE, pp. 155\u2013164. IEEE (1992)","DOI":"10.1109\/ICCL.1992.185478"},{"issue":"2","key":"154_CR7","doi-asserted-by":"crossref","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. Constr. J. 15(2), 238\u2013264 (2010)","journal-title":"Constr. J."},{"key":"154_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: Proceedings of the 1st Joint IEEE\/IFIP Symposium on Theoretical Aspects of Software Engineering, IEEE, pp. 3\u201320. IEEE (2007)","DOI":"10.1109\/TASE.2007.55"},{"key":"154_CR9","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the POPL, pp. 238\u2013252. ACM, (1977)","DOI":"10.1145\/512950.512973"},{"key":"154_CR10","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Proceedings of the POPL, pp. 269\u2013282. ACM Press, (1979)","DOI":"10.1145\/567752.567778"},{"key":"154_CR11","doi-asserted-by":"crossref","unstructured":"Cousot, P.: Abstract interpretation based formal methods and future challenges. In: Wilhelm, R. (ed) Informatics-10 Years Back. 10 Years Ahead, Lecture Notes in Computer Science, vol. 2000, pp. 138\u2013156. Springer, Berlin (2001)","DOI":"10.1007\/3-540-44577-3_10"},{"key":"154_CR12","doi-asserted-by":"crossref","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: Proceedings of the FMICS, LNCS, vol. 5825, pp. 53\u201369. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-04570-7_6"},{"key":"154_CR13","doi-asserted-by":"crossref","unstructured":"Denmat, T., Gotlieb, A., Ducass\u00e9, M.: An abstract interpretation based combinator for modeling while loops in constraint programming. In: Proceedings of the Principles and Practices of Constraint Programming (CP\u201907), LNCS, vol. 4741, pp. 241\u2013255. Springer Verlag, Berlin (2007)","DOI":"10.1007\/978-3-540-74970-7_19"},{"issue":"2","key":"154_CR14","doi-asserted-by":"crossref","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 Trans. Comput. 60(2), 242\u2013253 (2011)","journal-title":"IEEE Trans. Comput."},{"key":"154_CR15","doi-asserted-by":"crossref","unstructured":"D\u2019Silva, V., Haller, L., Kroening, D., Tautschnig, M.: Numeric bounds analysis with conflict-driven learning. In: Proceedings of the TACAS, Lecture Notes in Computer Science, vol. 7214, pp. 48\u201363. Springer, Berlin (2012)","DOI":"10.1007\/978-3-642-28756-5_5"},{"key":"154_CR16","doi-asserted-by":"crossref","unstructured":"Ghorbal, K., Goubault, E., Putot, S.: A logical product approach to zonotope intersection. In: Proceedings of the CAV, LNCS, vol. 6174, pp. 212\u2013226. Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-14295-6_22"},{"key":"154_CR17","doi-asserted-by":"crossref","unstructured":"Girard, A.: Reachability of uncertain linear systems using zonotopes. In: Proceedings of the HSCC, Lecture Notes in Computer Science, vol. 3414, pp. 291\u2013305. Springer, Berlin, (2005)","DOI":"10.1007\/978-3-540-31954-2_19"},{"issue":"1","key":"154_CR18","doi-asserted-by":"crossref","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 Comput. Surv. 23(1), 5\u201348 (1991)","journal-title":"ACM Comput. Surv."},{"key":"154_CR19","doi-asserted-by":"crossref","unstructured":"Goubault, E., Putot, S.: Static analysis of numerical algorithms. In: Proceedings of the SAS, LNCS, vol. 4134, pp. 18\u201334. Springer, Berlin (2006)","DOI":"10.1007\/11823230_3"},{"issue":"1","key":"154_CR20","doi-asserted-by":"crossref","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 Trans. Math. Softw. 32(1), 138\u2013156 (2006)","journal-title":"ACM Trans. Math. Softw."},{"key":"154_CR21","doi-asserted-by":"crossref","unstructured":"Harrison, J.: A machine-checked theory of floating-point arithmetic. TPHOLs, LNCS, vol. 1690, pp. 113\u2013130. Springer-Verlag, Berlin (1999)","DOI":"10.1007\/3-540-48256-3_9"},{"key":"154_CR22","doi-asserted-by":"crossref","first-page":"797","DOI":"10.1137\/S0036142995281504","volume":"34","author":"PV Hentenryck","year":"1997","unstructured":"Hentenryck, P.V., Mcallester, D., Kapur, D.: Solving polynomial systems using a branch and prune approach. SIAM J. Numer. Ana. 34, 797\u2013827 (1997)","journal-title":"SIAM J. Numer. Ana."},{"key":"154_CR23","unstructured":"Lhomme, O.: Consistency techniques for numeric CSPs. In: Proceedings of the 13th International Joint Conference on Artificial Intelligence, pp. 232\u2013238. Morgan Kaufmann Publishers Inc., Burlington (1993)"},{"key":"154_CR24","doi-asserted-by":"crossref","unstructured":"Marre, B., Michel, C.: Improving the floating point addition and subtraction constraints. In: Proceedings of the CP, LNCS, vol. 6308, pp. 360\u2013367. Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-15396-9_30"},{"key":"154_CR25","doi-asserted-by":"crossref","unstructured":"Michel, C., Rueher, M., Lebbah, Y.: Solving constraints over floating-point numbers. In: Principles and Practice of Constraint Programming\u2014CP, LNCS, vol. 2239, pp. 524\u2013538. Springer Verlag, Berlin (2001)","DOI":"10.1007\/3-540-45578-7_36"},{"key":"154_CR26","unstructured":"Michel, C.: Exact projection functions for floating-point number constraints. In: Proceedings of the 7th International Symposium on Artificial Intelligence and Mathematics. (2002)"},{"key":"154_CR27","doi-asserted-by":"crossref","unstructured":"Pelleau, M., Min\u00e9, A., Truchet, C., Benhamou, F.: A constraint solver based on abstract domains. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds) 14th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2013), Lecture Notes in Computer Science, vol. 7737, pp. 434\u2013454. Springer, Berlin (2013)","DOI":"10.1007\/978-3-642-35873-9_26"},{"key":"154_CR28","unstructured":"Rossi, F., van Beek, P., Walsh, T. (eds.): Handbook of Constraint Programming, 1st edn. Elsevier Science, Amsterdam (2006)"}],"container-title":["Automated Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10515-014-0154-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10515-014-0154-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10515-014-0154-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,10]],"date-time":"2019-08-10T14:10:54Z","timestamp":1565446254000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10515-014-0154-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,5,22]]},"references-count":28,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2016,6]]}},"alternative-id":["154"],"URL":"https:\/\/doi.org\/10.1007\/s10515-014-0154-2","relation":{},"ISSN":["0928-8910","1573-7535"],"issn-type":[{"value":"0928-8910","type":"print"},{"value":"1573-7535","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,5,22]]}}}