{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T14:05:08Z","timestamp":1742911508238,"version":"3.40.3"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319194578"},{"type":"electronic","value":"9783319194585"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-19458-5_3","type":"book-chapter","created":{"date-parts":[[2015,5,11]],"date-time":"2015-05-11T11:41:14Z","timestamp":1431344474000},"page":"31-46","source":"Crossref","is-referenced-by-count":14,"title":["Intra-procedural Optimization of the Numerical Accuracy of Programs"],"prefix":"10.1007","author":[{"given":"Nasrine","family":"Damouche","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Matthieu","family":"Martel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexandre","family":"Chapoutot","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"3_CR1","unstructured":"ANSI\/IEEE. IEEE Standard for Binary Floating-Point Arithmetic. SIAM (2008)"},{"key":"3_CR2","doi-asserted-by":"crossref","unstructured":"Appel, A.-W.: Modern Compiler Implementation in ML. Cambridge University Press (1998)","DOI":"10.1017\/CBO9780511811449"},{"key":"3_CR3","doi-asserted-by":"crossref","unstructured":"Barr, E.-T., Vo, T., Le, V., Su, Z.: Automatic detection of floating-point exceptions. In: Symposium on Principles of Programming Languages, POPL 2013, pp. 549\u2013560. ACM (2013)","DOI":"10.1145\/2480359.2429133"},{"key":"3_CR4","doi-asserted-by":"crossref","unstructured":"Benz, F., Hildebrandt, A., Hack, S.: A dynamic program analysis to find floating-point accuracy problems. In: Programming Language Design and Implementation, PLDI 2012, pp. 453\u2013462. ACM (2012)","DOI":"10.1145\/2345156.2254118"},{"issue":"1","key":"3_CR5","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1921532.1921553","volume":"36","author":"J. Bertrane","year":"2011","unstructured":"Bertrane, J., Cousot, P., Cousot, R., Feret, F., Mauborgne, L., Min\u00e9, A., Rival, X.: Static analysis by abstract interpretation of embedded critical software. ACM SIGSOFT Software Engineering Notes\u00a036(1), 1\u20138 (2011)","journal-title":"ACM SIGSOFT Software Engineering Notes"},{"key":"3_CR6","doi-asserted-by":"crossref","unstructured":"Chapoutot, A., Damouche, N., Martel, M.: Automatic transformation of a PID controller. In: International Workshop on Numerical Software Verification (2014)","DOI":"10.1016\/j.entcs.2015.10.006"},{"key":"3_CR7","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: Principles of Programming Languages, pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"key":"3_CR8","doi-asserted-by":"crossref","unstructured":"Cousout, P., Cousot, R.: Systematic design of program transformation frameworks by abstract interpretation. In: Principles of Programming Languages, pp. 178\u2013190. ACM (2002)","DOI":"10.1145\/565816.503290"},{"key":"3_CR9","doi-asserted-by":"crossref","unstructured":"Cytron, R., Gershbein, R.: Efficient accomodation of may-alias information in SSA form. In: Programming Language Design and Implementation (PLDI), pp. 36\u201345. ACM (1993)","DOI":"10.1145\/173262.155094"},{"key":"3_CR10","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)"},{"issue":"6","key":"3_CR11","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1109\/MCS.2010.938196","volume":"30","author":"E. Feron","year":"2010","unstructured":"Feron, E.: From control systems to control software. IEEE Control Systems Magazine\u00a030(6), 50\u201371 (2010)","journal-title":"IEEE Control Systems Magazine"},{"key":"3_CR12","doi-asserted-by":"crossref","unstructured":"Gao, X., Bayliss, S., Constantinides, G.-A.: SOAP: structural optimization of arithmetic expressions for high-level synthesis. In: Field-Programmable Technology, FPT, pp. 112\u2013119. IEEE (2013)","DOI":"10.1109\/FPT.2013.6718340"},{"key":"3_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-38856-9_1","volume-title":"Static Analysis","author":"E. Goubault","year":"2013","unstructured":"Goubault, E.: Static analysis by abstract interpretation of numerical programs and systems, and FLUCTUAT. In: Logozzo, F., F\u00e4hndrich, M. (eds.) SAS 2013. LNCS, vol.\u00a07935, pp. 1\u20133. Springer, Heidelberg (2013)"},{"key":"3_CR14","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)"},{"key":"3_CR15","doi-asserted-by":"crossref","DOI":"10.1093\/oso\/9780198538417.001.0001","volume-title":"Lambda Calculi A Guide For Computer Scientists","author":"E. Hankin","year":"1994","unstructured":"Hankin, E.: Lambda Calculi A Guide For Computer Scientists. Clarendon Press, Oxford (1994)"},{"key":"3_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1007\/978-3-642-33125-1_8","volume-title":"Static Analysis","author":"A. Ioualalen","year":"2012","unstructured":"Ioualalen, A., Martel, M.: A new abstract domain for the representation of mathematically equivalent expressions. In: Min\u00e9, A., Schmidt, D. (eds.) SAS 2012. LNCS, vol.\u00a07460, pp. 75\u201393. Springer, Heidelberg (2012)"},{"key":"3_CR17","doi-asserted-by":"crossref","unstructured":"Ioualalen, A., Martel, M.: Synthesizing accurate floating-point formulas. In: Application-Specific Systems, Architectures and Processors, ASAP, pp. 113\u2013116 (2013)","DOI":"10.1109\/ASAP.2013.6567563"},{"issue":"3","key":"3_CR18","doi-asserted-by":"publisher","first-page":"480","DOI":"10.1145\/243439.243447","volume":"28","author":"N.-D. Jones","year":"1996","unstructured":"Jones, N.-D.: An introduction to partial evaluation. ACM Computing Surveys\u00a028(3), 480\u2013503 (1996)","journal-title":"ACM Computing Surveys"},{"key":"3_CR19","unstructured":"Kendall, A.: An Introduction to Numerical Analysis. John Wiley & Sons (1989)"},{"key":"3_CR20","doi-asserted-by":"crossref","unstructured":"Logozzo, F., Ball, T.: Modular and verified automatic program repair. In: Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA, pp. 133\u2013146. ACM (2012)","DOI":"10.1145\/2398857.2384626"},{"key":"3_CR21","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.entcs.2012.09.002","volume":"287","author":"M. Martel","year":"2012","unstructured":"Martel, M.: Accurate evaluation of arithmetic expressions (invited talk). Electr. Notes Theor. Comput. Sci.\u00a0287, 3\u201316 (2012)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"issue":"1","key":"3_CR22","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1007\/s10990-006-8608-2","volume":"19","author":"M. Martel","year":"2006","unstructured":"Martel, M.: Semantics of roundoff error propagation in finite precision calculations. Higher-Order and Symbolic Computation\u00a019(1), 7\u201330 (2006)","journal-title":"Higher-Order and Symbolic Computation"},{"key":"3_CR23","doi-asserted-by":"crossref","unstructured":"Muller, J.-M., Brisebarre, N., De Dinechin, F., Jeannerod, C.-P., Lef\u00e8vre, V., Melquiond, G., Revol, N., Stehl\u00e9, D., Torres, S.: Handbook of Floating-Point Arithmetic. Birkh\u00e4user (2010)","DOI":"10.1007\/978-0-8176-4705-6"},{"key":"3_CR24","doi-asserted-by":"crossref","unstructured":"Tate, R., Stepp, M., Tatlock, Z., Lerner, S.: Equality saturation: A new approach to optimization. Logical Methods in Computer Science 7(1) (2011)","DOI":"10.2168\/LMCS-7(1:10)2011"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Industrial Critical Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-19458-5_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,6,8]],"date-time":"2024-06-08T22:30:20Z","timestamp":1717885820000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-19458-5_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319194578","9783319194585"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-19458-5_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}