{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,1]],"date-time":"2026-04-01T22:31:02Z","timestamp":1775082662215,"version":"3.50.1"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030349677","type":"print"},{"value":"9783030349684","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-34968-4_18","type":"book-chapter","created":{"date-parts":[[2019,11,22]],"date-time":"2019-11-22T00:14:54Z","timestamp":1574381694000},"page":"322-340","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":13,"title":["Sound Probabilistic Numerical Error Analysis"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8639-4116","authenticated-orcid":false,"given":"Debasmita","family":"Lohar","sequence":"first","affiliation":[]},{"given":"Milos","family":"Prokop","sequence":"additional","affiliation":[]},{"given":"Eva","family":"Darulova","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,11,22]]},"reference":[{"key":"18_CR1","unstructured":"IEEE Standard for Floating-Point Arithmetic. IEEE Std 754-2008 (2008)"},{"key":"18_CR2","unstructured":"GLPK (2012). https:\/\/www.gnu.org\/software\/glpk\/"},{"key":"18_CR3","unstructured":"Project Sklearn-porter (2018). https:\/\/github.com\/nok\/sklearn-porter"},{"issue":"2\u20134","key":"18_CR4","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/s00607-011-0182-8","volume":"94","author":"O Bouissou","year":"2012","unstructured":"Bouissou, O., Goubault, E., Goubault-Larrecq, J., Putot, S.: A generalization of p-boxes to affine arithmetic. Computing 94(2\u20134), 189\u2013201 (2012)","journal-title":"Computing"},{"key":"18_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/978-3-662-49674-9_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"O Bouissou","year":"2016","unstructured":"Bouissou, O., Goubault, E., Putot, S., Chakarov, A., Sankaranarayanan, S.: Uncertainty propagation using probabilistic affine forms and concentration of measure inequalities. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 225\u2013243. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49674-9_13"},{"issue":"1","key":"18_CR6","first-page":"1","volume":"76","author":"B Carpenter","year":"2017","unstructured":"Carpenter, B., et al.: Stan: a probabilistic programming language. J. Stat. Softw. Art. 76(1), 1\u201332 (2017)","journal-title":"J. Stat. Softw. Art."},{"issue":"4","key":"18_CR7","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. Int. J. Softw. Tools Technol. Transfer 19(4), 427\u2013448 (2017)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"18_CR8","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). https:\/\/doi.org\/10.1007\/978-3-319-89960-2_15"},{"issue":"2","key":"18_CR9","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"},{"issue":"3","key":"18_CR10","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/s11334-010-0128-x","volume":"6","author":"M Daumas","year":"2010","unstructured":"Daumas, M., Lester, D., Martin-Dorel, E., Truffert, A.: Improved bound for stochastic formal correctness of numerical algorithms. Innovations Syst. Softw. Eng. 6(3), 173\u2013179 (2010)","journal-title":"Innovations Syst. Softw. Eng."},{"key":"18_CR11","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":"18_CR12","unstructured":"Dhiflaoui, M., et al.: Certifying and repairing solutions to large LPs. How good are LP-solvers? In: SODA, pp. 255\u2013256 (2003)"},{"key":"18_CR13","doi-asserted-by":"crossref","unstructured":"Ferson, S., Kreinovich, V., Ginzburg, L., Myers, D.S., Sentz, K.: Constructing probability boxes and Dempster-Shafer structures. Technical report, Sandia National Laboratories (2003)","DOI":"10.2172\/809606"},{"issue":"1\u20134","key":"18_CR14","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":"18_CR15","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). https:\/\/doi.org\/10.1007\/978-3-642-18275-4_17"},{"key":"18_CR16","doi-asserted-by":"crossref","unstructured":"Izycheva, A., Darulova, E.: On sound relative error bounds for floating-point arithmetic. In: FMCAD (2017)","DOI":"10.23919\/FMCAD.2017.8102236"},{"key":"18_CR17","unstructured":"Keil, C.: Lurupa - rigorous error bounds in linear programming. In: Algebraic and Numerical Algorithms and Computer-assisted Proofs. No. 05391 in Dagstuhl Seminar Proceedings (2006). http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2006\/445"},{"key":"18_CR18","doi-asserted-by":"crossref","unstructured":"Lohar, D., Darulova, E., Putot, S., Goubault, E.: Discrete choice in the presence of numerical uncertainties. In: EMSOFT (2018)","DOI":"10.1109\/TCAD.2018.2857320"},{"issue":"4","key":"18_CR19","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":"18_CR20","unstructured":"Minka, T., et al.: Infer.NET 2.6 (2014). http:\/\/research.microsoft.com\/infernet"},{"key":"18_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1007\/978-3-319-41528-4_4","volume-title":"Computer Aided Verification","author":"T Gehr","year":"2016","unstructured":"Gehr, T., Misailovic, S., Vechev, M.: PSI: exact symbolic inference for probabilistic programs. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 62\u201383. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_4"},{"key":"18_CR22","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":"18_CR23","volume-title":"Interval Analysis","author":"R Moore","year":"1966","unstructured":"Moore, R.: Interval Analysis. Prentice-Hall, Upper Saddle River (1966)"},{"key":"18_CR24","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). https:\/\/doi.org\/10.1007\/978-3-319-66266-4_14"},{"key":"18_CR25","doi-asserted-by":"crossref","unstructured":"Nori, A.V., Hur, C.K., Rajamani, S.K., Samuel, S.: R2: an efficient MCMC sampler for probabilistic programs. In: AAAI (2014)","DOI":"10.1609\/aaai.v28i1.9060"},{"key":"18_CR26","doi-asserted-by":"crossref","unstructured":"Sampson, A., Panchekha, P., Mytkowicz, T., McKinley, K.S., Grossman, D., Ceze, L.: Expressing and verifying probabilistic assertions. In: PLDI (2014)","DOI":"10.1145\/2594291.2594294"},{"key":"18_CR27","doi-asserted-by":"crossref","unstructured":"Sampson, A., Dietl, W., Fortuna, E., Gnanapragasam, D., Ceze, L., Grossman, D.: EnerJ: approximate data types for safe and general low-power computation. In: PLDI (2011)","DOI":"10.1145\/1993498.1993518"},{"key":"18_CR28","doi-asserted-by":"crossref","unstructured":"Sankaranarayanan, S., Chakarov, A., Gulwani, S.: Static analysis for probabilistic programs: inferring whole program properties from finitely many paths. In: PLDI (2013)","DOI":"10.1145\/2491956.2462179"},{"issue":"8","key":"18_CR29","doi-asserted-by":"publisher","first-page":"507","DOI":"10.1016\/j.cpc.2007.01.005","volume":"176","author":"NS Scott","year":"2007","unstructured":"Scott, N.S., J\u00e9z\u00e9quel, F., Denis, C., Chesneaux, J.M.: Numerical \u2018health check\u2019 for scientific codes: the CADNA approach. Comput. Phys. Commun. 176(8), 507\u2013521 (2007)","journal-title":"Comput. Phys. Commun."},{"key":"18_CR30","doi-asserted-by":"crossref","DOI":"10.1515\/9780691214696","volume-title":"A Mathematical Theory of Evidence","author":"G Shafer","year":"1976","unstructured":"Shafer, G.: A Mathematical Theory of Evidence. Princeton University Press, Princeton (1976)"},{"key":"18_CR31","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":"18_CR32","doi-asserted-by":"crossref","unstructured":"Tang, E., Barr, E., Li, X., Su, Z.: Perturbing numerical calculations for statistical analysis of floating-point program (in)stability. In: ISSTA (2010)","DOI":"10.1145\/1831708.1831724"},{"issue":"1","key":"18_CR33","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"}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-34968-4_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,10,6]],"date-time":"2022-10-06T17:23:42Z","timestamp":1665077022000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-34968-4_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030349677","9783030349684"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-34968-4_18","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":"22 November 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"IFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Integrated Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Bergen","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Norway","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":"2 December 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 December 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ifm2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/ifm2019.hvl.no\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}