{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T20:15:13Z","timestamp":1784232913424,"version":"3.55.0"},"publisher-location":"Cham","reference-count":48,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030317836","type":"print"},{"value":"9783030317843","type":"electronic"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"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":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-31784-3_17","type":"book-chapter","created":{"date-parts":[[2019,10,20]],"date-time":"2019-10-20T21:32:04Z","timestamp":1571607124000},"page":"294-313","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Synthesizing Efficient Low-Precision Kernels"],"prefix":"10.1007","author":[{"given":"Anastasiia","family":"Izycheva","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Eva","family":"Darulova","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Helmut","family":"Seidl","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2019,10,21]]},"reference":[{"key":"17_CR1","unstructured":"Project CORPIN. \nhttps:\/\/www-sop.inria.fr\/corpin\/logiciels\/ALIAS\/Benches\/"},{"key":"17_CR2","unstructured":"Python sklearn - multi-layer perceptron regressor (2019). \nhttps:\/\/scikit-learn.org\/stable\/modules\/generated\/sklearn.neural_network.MLPRegressor.html"},{"key":"17_CR3","doi-asserted-by":"crossref","unstructured":"Alur, R., et al.: Syntax-guided synthesis. In: FMCAD, pp. 1\u20138. IEEE (2013)","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"17_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/978-3-662-54577-5_18","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Alur","year":"2017","unstructured":"Alur, R., Radhakrishna, A., Udupa, A.: Scaling enumerative program synthesis via divide and conquer. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 319\u2013336. Springer, Heidelberg (2017). \nhttps:\/\/doi.org\/10.1007\/978-3-662-54577-5_18"},{"key":"17_CR5","doi-asserted-by":"crossref","unstructured":"Ansel, J., Wong, Y.L., Chan, C., Olszewski, M., Edelman, A., Amarasinghe, S.: Language and compiler support for auto-tuning variable-accuracy algorithms. In: CGO (2011)","DOI":"10.1109\/CGO.2011.5764677"},{"issue":"5","key":"17_CR6","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/s10009-013-0287-9","volume":"15","author":"R Bodik","year":"2013","unstructured":"Bodik, R., Jobstmann, B.: Algorithmic program synthesis: introduction. STTT 15(5), 397\u2013411 (2013)","journal-title":"STTT"},{"issue":"1","key":"17_CR7","doi-asserted-by":"publisher","first-page":"775","DOI":"10.1145\/2914770.2837666","volume":"51","author":"James Bornholt","year":"2016","unstructured":"Bornholt, J., Torlak, E., Grossman, D., Ceze, L.: Optimizing Synthesis with Metasketches. In: POPL (2016)","journal-title":"ACM SIGPLAN Notices"},{"key":"17_CR8","doi-asserted-by":"crossref","unstructured":"Brunie, N., De Dinechin, F., Kupriianova, O., Lauter, C.: Code generators for mathematical functions. In: ARITH (2015)","DOI":"10.1109\/ARITH.2015.22"},{"key":"17_CR9","doi-asserted-by":"crossref","unstructured":"Chiang, W.F., Baranowski, M., Briggs, I., Solovyev, A., Gopalakrishnan, G., Rakamari\u0107, Z.: Rigorous floating-point mixed-precision tuning. In: POPL (2017)","DOI":"10.1145\/3009837.3009846"},{"key":"17_CR10","doi-asserted-by":"crossref","unstructured":"Damouche, N., Martel, M.: Mixed precision tuning with salsa. In: PECCS, pp. 185\u2013194. SciTePress (2018)","DOI":"10.5220\/0006915500470056"},{"issue":"4","key":"17_CR11","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/s10009-016-0435-0","volume":"19","author":"N Damouche","year":"2017","unstructured":"Damouche, N., Martel, M., Chapoutot, A.: Improving the numerical accuracy of programs by automatic transformation. STTT 19(4), 427\u2013448 (2017)","journal-title":"STTT"},{"key":"17_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1007\/978-3-319-41540-6_21","volume-title":"Computer Aided Verification","author":"L D\u2019Antoni","year":"2016","unstructured":"D\u2019Antoni, L., Samanta, R., Singh, R.: Qlose: program repair with quantitative objectives. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 383\u2013401. Springer, Cham (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-319-41540-6_21"},{"key":"17_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-030-25543-5_11","volume-title":"Computer Aided Verification","author":"E Darulova","year":"2019","unstructured":"Darulova, E., Volkova, A.: Sound approximation of programs with elementary functions. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11562, pp. 174\u2013183. Springer, Cham (2019). \nhttps:\/\/doi.org\/10.1007\/978-3-030-25543-5_11"},{"key":"17_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"270","DOI":"10.1007\/978-3-319-89960-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Darulova","year":"2018","unstructured":"Darulova, E., Izycheva, A., Nasir, F., Ritter, F., Becker, H., Bastian, R.: Daisy - framework for analysis and optimization of numerical programs (tool paper). In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10805, pp. 270\u2013287. Springer, Cham (2018). \nhttps:\/\/doi.org\/10.1007\/978-3-319-89960-2_15"},{"issue":"2","key":"17_CR15","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1145\/3014426","volume":"39","author":"E Darulova","year":"2017","unstructured":"Darulova, E., Kuncak, V.: Towards a compiler for reals. TOPLAS 39(2), 8 (2017)","journal-title":"TOPLAS"},{"key":"17_CR16","doi-asserted-by":"crossref","unstructured":"Darulova, E., Sharma, S., Horn, E.: Sound mixed-precision optimization with rewriting. In: ICCPS (2018)","DOI":"10.1109\/ICCPS.2018.00028"},{"key":"17_CR17","doi-asserted-by":"crossref","unstructured":"De Dinechin, F., Lauter, C.Q., Melquiond, G.: Assisted verification of elementary functions using Gappa. In: ACM Symposium on Applied Computing (2006)","DOI":"10.1145\/1141277.1141584"},{"key":"17_CR18","doi-asserted-by":"crossref","unstructured":"Esmaeilzadeh, H., Sampson, A., Ceze, L., Burger, D.: Neural acceleration for general-purpose approximate programs. In: MICRO (2012)","DOI":"10.1109\/MICRO.2012.48"},{"key":"17_CR19","doi-asserted-by":"crossref","unstructured":"Feng, Y., Martins, R., Wang, Y., Dillig, I., Reps, T.W.: Component-based synthesis for complex APIs. In: POPL (2017)","DOI":"10.1145\/3009837.3009851"},{"issue":"1\u20134","key":"17_CR20","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1023\/B:NUMA.0000049462.70970.b6","volume":"37","author":"LH Figueiredo de","year":"2004","unstructured":"de Figueiredo, L.H., Stolfi, J.: Affine arithmetic: concepts and applications. Numer. Algorithms 37(1\u20134), 147\u2013158 (2004)","journal-title":"Numer. Algorithms"},{"key":"17_CR21","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. 6538, pp. 232\u2013247. Springer, Heidelberg (2011). \nhttps:\/\/doi.org\/10.1007\/978-3-642-18275-4_17"},{"issue":"1","key":"17_CR22","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1145\/1925844.1926423","volume":"46","author":"Sumit Gulwani","year":"2011","unstructured":"Gulwani, S.: Automating string processing in spreadsheets using input-output examples. In: POPL (2011)","journal-title":"ACM SIGPLAN Notices"},{"key":"17_CR23","unstructured":"IEEE: IEEE Standard for Floating-Point Arithmetic. IEEE Std 754\u20132008 (2008)"},{"key":"17_CR24","doi-asserted-by":"crossref","unstructured":"Kneuss, E., Kuraj, I., Kuncak, V., Suter, P.: Synthesis modulo recursive functions. In: OOPSLA (2013)","DOI":"10.1145\/2509136.2509555"},{"key":"17_CR25","doi-asserted-by":"crossref","unstructured":"Kuncak, V., Mayer, M., Piskac, R., Suter, P.: Complete functional synthesis. In: PLDI (2010)","DOI":"10.1145\/1806596.1806632"},{"key":"17_CR26","doi-asserted-by":"crossref","unstructured":"Kupriianova, O., Lauter, C.: A domain splitting algorithm for the mathematical functions code generator. In: Asilomar (2014)","DOI":"10.1109\/ACSSC.2014.7094664"},{"key":"17_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"713","DOI":"10.1007\/978-3-662-44199-2_106","volume-title":"Mathematical Software \u2013 ICMS 2014","author":"O Kupriianova","year":"2014","unstructured":"Kupriianova, O., Lauter, C.: Metalibm: a mathematical functions code generator. In: Hong, H., Yap, C. (eds.) ICMS 2014. LNCS, vol. 8592, pp. 713\u2013717. Springer, Heidelberg (2014). \nhttps:\/\/doi.org\/10.1007\/978-3-662-44199-2_106"},{"issue":"10","key":"17_CR28","first-page":"1990","volume":"25","author":"DU Lee","year":"2006","unstructured":"Lee, D.U., Gaffar, A.A., Cheung, R.C., Mencer, O., Luk, W., Constantinides, G.A.: Accuracy-guaranteed bit-width optimization. TCAD 25(10), 1990\u20132000 (2006)","journal-title":"TCAD"},{"key":"17_CR29","doi-asserted-by":"crossref","unstructured":"Lee, S., John, L.K., Gerstlauer, A.: High-level synthesis of approximate hardware under joint precision and voltage scaling. In: DATE, pp. 187\u2013192 (2017)","DOI":"10.23919\/DATE.2017.7926980"},{"issue":"POPL","key":"17_CR30","first-page":"47","volume":"2","author":"W Lee","year":"2018","unstructured":"Lee, W., Sharma, R., Aiken, A.: On automatically proving the correctness of math.h implementations. Proc. ACM Program. Lang. 2(POPL), 47 (2018)","journal-title":"Proc. ACM Program. Lang."},{"key":"17_CR31","first-page":"2381","volume":"37","author":"D Lohar","year":"2018","unstructured":"Lohar, D., Darulova, E., Putot, S., Goubault, E.: Discrete choice in the presence of numerical uncertainties. IEEE TCAD 37, 2381\u20132392 (2018)","journal-title":"IEEE TCAD"},{"issue":"6","key":"17_CR32","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1145\/2980983.2908122","volume":"51","author":"C Loncaric","year":"2016","unstructured":"Loncaric, C., Torlak, E., Ernst, M.D.: Fast synthesis of fast collections. ACM SIGPLAN Not. 51(6), 355\u2013368 (2016)","journal-title":"ACM SIGPLAN Not."},{"issue":"4","key":"17_CR33","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1145\/3015465","volume":"43","author":"V Magron","year":"2017","unstructured":"Magron, V., Constantinides, G., Donaldson, A.: Certified roundoff error bounds using semidefinite programming. ACM Trans. Math. Softw. 43(4), 34 (2017)","journal-title":"ACM Trans. Math. Softw."},{"key":"17_CR34","doi-asserted-by":"crossref","unstructured":"Misailovic, S., Carbin, M., Achour, S., Qi, Z., Rinard, M.C.: Chisel: reliability- and accuracy-aware optimization of approximate computational kernels. In: OOPSLA (2014)","DOI":"10.1145\/2660193.2660231"},{"key":"17_CR35","volume-title":"Interval Analysis","author":"R Moore","year":"1966","unstructured":"Moore, R.: Interval Analysis. Prentice-Hall, Upper Saddle River (1966)"},{"key":"17_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/978-3-319-66266-4_14","volume-title":"Computer Safety, Reliability, and Security","author":"M Moscato","year":"2017","unstructured":"Moscato, M., Titolo, L., Dutle, A., Mu\u00f1oz, C.A.: Automatic estimation of verified floating-point round-off errors via static analysis. In: Tonetta, S., Schoitsch, E., Bitsch, F. (eds.) SAFECOMP 2017. LNCS, vol. 10488, pp. 213\u2013229. Springer, Cham (2017). \nhttps:\/\/doi.org\/10.1007\/978-3-319-66266-4_14"},{"key":"17_CR37","doi-asserted-by":"crossref","unstructured":"Briesbarre, N., Chevillard, S.: Efficient polynomial l-approximations. In: ARITH (2007)","DOI":"10.1109\/ARITH.2007.17"},{"issue":"2","key":"17_CR38","doi-asserted-by":"publisher","first-page":"10:1","DOI":"10.1145\/3173545","volume":"19","author":"D Neider","year":"2018","unstructured":"Neider, D., Saha, S., Madhusudan, P.: Compositional synthesis of piece-wise functions by learning classifiers. ACM Trans. Comput. Logic 19(2), 10:1\u201310:23 (2018)","journal-title":"ACM Trans. Comput. Logic"},{"issue":"6","key":"17_CR39","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1145\/2813885.2737982","volume":"50","author":"Aditya V. Nori","year":"2015","unstructured":"Nori, A.V., Ozair, S., Rajamani, S.K., Vijaykeerthy, D.: Efficient synthesis of probabilistic programs. In: PLDI. ACM (2015)","journal-title":"ACM SIGPLAN Notices"},{"key":"17_CR40","doi-asserted-by":"crossref","unstructured":"Braojos, R., Ansaloni, G., Atienza, D.: A methodology for embedded classification of heartbeats using random projections. In: DATE. EPFL (2013)","DOI":"10.7873\/DATE.2013.189"},{"key":"17_CR41","doi-asserted-by":"crossref","unstructured":"Renganarayana, L., Srinivasan, V., Nair, R., Prener, D.: Programming with relaxed synchronization. In: RACES, pp. 41\u201350 (2012)","DOI":"10.1145\/2414729.2414737"},{"key":"17_CR42","doi-asserted-by":"crossref","unstructured":"Schkufza, E., Sharma, R., Aiken, A.: Stochastic optimization of floating-point programs with tunable precision. In: PLDI (2014)","DOI":"10.1145\/2594291.2594302"},{"key":"17_CR43","doi-asserted-by":"crossref","unstructured":"Sidiroglou-Douskos, S., Misailovic, S., Hoffmann, H., Rinard, M.: Managing performance vs. accuracy trade-offs with loop perforation. In: ESEC\/FSE (2011)","DOI":"10.1145\/2025113.2025133"},{"key":"17_CR44","doi-asserted-by":"crossref","unstructured":"Solovyev, A., Jacobsen, C., Rakamaric, Z., Gopalakrishnan, G.: Rigorous estimation of floating-point round-off errors with symbolic taylor expansions. In: FM (2015)","DOI":"10.1007\/978-3-319-19249-9_33"},{"key":"17_CR45","unstructured":"Xilinx: Vivado design suite (2018). \nhttps:\/\/www.xilinx.com\/products\/design-tools\/vivado.html"},{"issue":"1","key":"17_CR46","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1109\/MDAT.2015.2505723","volume":"33","author":"Q Xu","year":"2016","unstructured":"Xu, Q., Mytkowicz, T., Kim, N.S.: Approximate computing: a survey. IEEE Des. Test 33(1), 8\u201322 (2016)","journal-title":"IEEE Des. Test"},{"issue":"2","key":"17_CR47","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1109\/MDAT.2016.2630270","volume":"34","author":"A Yazdanbakhsh","year":"2017","unstructured":"Yazdanbakhsh, A., Mahajan, D., Esmaeilzadeh, H., Lotfi-Kamran, P.: AxBench: a multiplatform benchmark suite for approximate computing. IEEE Des. Test 34(2), 60\u201368 (2017)","journal-title":"IEEE Des. Test"},{"key":"17_CR48","doi-asserted-by":"crossref","unstructured":"Yi, X., Chen, L., Mao, X., Ji, T.: Efficient automated repair of high floating-point errors in numerical libraries. In: POPL (2019)","DOI":"10.1145\/3290369"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-31784-3_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,11,14]],"date-time":"2019-11-14T13:30:01Z","timestamp":1573738201000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-31784-3_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030317836","9783030317843"],"references-count":48,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-31784-3_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"21 October 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ATVA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Automated Technology for Verification and Analysis","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Taipei","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Taiwan","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 October 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31 October 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"atva2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/atva2019.iis.sinica.edu.tw\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Open","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Easychair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"87","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"29","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"33% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.4","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Between 1 and 2","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}