{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:48:34Z","timestamp":1740098914417,"version":"3.37.3"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319635002"},{"type":"electronic","value":"9783319635019"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-63501-9_4","type":"book-chapter","created":{"date-parts":[[2017,7,11]],"date-time":"2017-07-11T09:23:01Z","timestamp":1499764981000},"page":"38-60","source":"Crossref","is-referenced-by-count":3,"title":["Sound Numerical Computations in Abstract Acceleration"],"prefix":"10.1007","author":[{"given":"Dario","family":"Cattaruzza","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5627-9093","authenticated-orcid":false,"given":"Alessandro","family":"Abate","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter","family":"Schrammel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Daniel","family":"Kroening","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,7,12]]},"reference":[{"key":"4_CR1","doi-asserted-by":"crossref","unstructured":"Anderson, E., Bai, Z., Dongarra, J., Greenbaum, A., McKenney, A., Du Croz, J., Hammerling, S., Demmel, J., Bischof, C., Sorensen, D.: Lapack: a portable linear algebra library for high-performance computers. In: Proceedings of the 1990 ACM\/IEEE Conference on Supercomputing, pp. 2\u201311. IEEE Computer Society Press (1990)","DOI":"10.1109\/SUPERC.1990.129995"},{"key":"4_CR2","doi-asserted-by":"crossref","unstructured":"Bak, S., Duggirala, P.S.: Hylaa: a tool for computing simulation-equivalent reachability for linear systems. In: Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control, HSCC 2017, Pittsburgh, PA, USA, 18\u201320 April 2017, pp. 173\u2013178 (2017)","DOI":"10.1145\/3049797.3049808"},{"key":"4_CR3","doi-asserted-by":"crossref","unstructured":"Bouissou, O., Mimram, S., Chapoutot, A.: Hyson: set-based simulation of hybrid systems. In: 2012 23rd IEEE International Symposium on Rapid System Prototyping (RSP), pp. 79\u201385. IEEE (2012)","DOI":"10.1109\/RSP.2012.6380694"},{"key":"4_CR4","unstructured":"Bradley, S., Hax, A., Magnanti, T.: Applied Mathematical Programming (1977)"},{"issue":"6","key":"4_CR5","doi-asserted-by":"crossref","first-page":"1150","DOI":"10.1109\/TFUZZ.2013.2265090","volume":"21","author":"H Bustince","year":"2013","unstructured":"Bustince, H., Galar, M., Bedregal, B., Kolesarova, A., Mesiar, R.: A new approach to interval-valued choquet integrals and the problem of ordering in interval-valued fuzzy set applications. IEEE Trans. Fuzzy Syst. 21(6), 1150\u20131162 (2013)","journal-title":"IEEE Trans. Fuzzy Syst."},{"key":"4_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1007\/978-3-662-48288-9_18","volume-title":"Static Analysis","author":"D Cattaruzza","year":"2015","unstructured":"Cattaruzza, D., Abate, A., Schrammel, P., Kroening, D.: Unbounded-time analysis of guarded LTI systems with inputs by abstract acceleration. In: Blazy, S., Jensen, T. (eds.) SAS 2015. LNCS, vol. 9291, pp. 312\u2013331. Springer, Heidelberg (2015). doi: 10.1007\/978-3-662-48288-9_18"},{"key":"4_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-540-89330-1_2","volume-title":"Programming Languages and Systems","author":"L Chen","year":"2008","unstructured":"Chen, L., Min\u00e9, A., Cousot, P.: A sound floating-point polyhedra abstract domain. In: Ramalingam, G. (ed.) APLAS 2008. LNCS, vol. 5356, pp. 3\u201318. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-89330-1_2"},{"key":"4_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/978-3-642-39799-8_18","volume-title":"Computer Aided Verification","author":"X Chen","year":"2013","unstructured":"Chen, X., \u00c1brah\u00e1m, E., Sankaranarayanan, S.: Flow*: an analyzer for non-linear hybrid systems. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 258\u2013263. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-39799-8_18"},{"key":"4_CR9","first-page":"159","volume":"3","author":"G Debreu","year":"1954","unstructured":"Debreu, G.: Representation of a preference ordering by a numerical function. Decis. Process. 3, 159\u2013165 (1954)","journal-title":"Decis. Process."},{"key":"4_CR10","unstructured":"Felsner, S.: Interval orders: combinatorial structure and algorithms. Technische Universit\u00e4t Berlin (1992)"},{"key":"4_CR11","volume-title":"Interval Orders and Interval Graphs - A Study of Partially Ordered Sets","author":"PC Fishburn","year":"1985","unstructured":"Fishburn, P.C.: Interval Orders and Interval Graphs - A Study of Partially Ordered Sets. Wiley, Hoboken (1985)"},{"issue":"2","key":"4_CR12","doi-asserted-by":"crossref","first-page":"13","DOI":"10.1145\/1236463.1236468","volume":"33","author":"L Fousse","year":"2007","unstructured":"Fousse, L., Hanrot, G., Lef\u00e8vre, V., P\u00e9lissier, P., Zimmermann, P.: MPFR: a multiple-precision binary floating-point library with correct rounding. ACM Trans. Math. Softw. (TOMS) 33(2), 13 (2007)","journal-title":"ACM Trans. Math. Softw. (TOMS)"},{"key":"4_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1007\/978-3-642-22110-1_30","volume-title":"Computer Aided Verification","author":"G Frehse","year":"2011","unstructured":"Frehse, G., et al.: SpaceEx: scalable verification of hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 379\u2013395. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-22110-1_30"},{"key":"4_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/3-540-61576-8_77","volume-title":"Combinatorics and Computer Science","author":"K Fukuda","year":"1996","unstructured":"Fukuda, K., Prodon, A.: Double description method revisited. In: Deza, M., Euler, R., Manoussakis, I. (eds.) CCS 1995. LNCS, vol. 1120, pp. 91\u2013111. Springer, Heidelberg (1996). doi: 10.1007\/3-540-61576-8_77"},{"issue":"3","key":"4_CR15","doi-asserted-by":"crossref","first-page":"449","DOI":"10.1287\/ijoc.2016.0692","volume":"28","author":"AM Gleixner","year":"2016","unstructured":"Gleixner, A.M., Steffy, D.E., Wolter, K.: Iterative refinement for linear programming. INFORMS J. Comput. 28(3), 449\u2013464 (2016)","journal-title":"INFORMS J. Comput."},{"issue":"1","key":"4_CR16","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. (CSUR) 23(1), 5\u201348 (1991)","journal-title":"ACM Comput. Surv. (CSUR)"},{"key":"4_CR17","unstructured":"Guennebaud, G., Jacob, B., et al.: Eigen v3 (2010) http:\/\/eigen.tuxfamily.org"},{"key":"4_CR18","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1016\/0024-3795(92)90016-4","volume":"172","author":"Y Hong","year":"1992","unstructured":"Hong, Y., Pan, C.T.: A lower bound for the smallest singular value. Linear Algebra Appl. 172, 27\u201332 (1992)","journal-title":"Linear Algebra Appl."},{"key":"4_CR19","unstructured":"IEEE Task P754: IEEE 754\u20132008, Standard for Floating-Point Arithmetic, August 2008"},{"key":"4_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"661","DOI":"10.1007\/978-3-642-02658-4_52","volume-title":"Computer Aided Verification","author":"B Jeannet","year":"2009","unstructured":"Jeannet, B., Min\u00e9, A.: Apron: a library of numerical abstract domains for static analysis. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 661\u2013667. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-02658-4_52"},{"key":"4_CR21","doi-asserted-by":"crossref","unstructured":"Jeannet, B., Schrammel, P., Sankaranarayanan, S.: Abstract acceleration of general linear loops. In: POPL, pp. 529\u2013540. ACM (2014)","DOI":"10.1145\/2535838.2535843"},{"key":"4_CR22","doi-asserted-by":"crossref","unstructured":"Laub, A.J.: Matrix Analysis for Scientists and Engineers. SIAM (2005)","DOI":"10.1137\/1.9780898717907"},{"issue":"3","key":"4_CR23","doi-asserted-by":"crossref","first-page":"308","DOI":"10.1145\/355841.355847","volume":"5","author":"CL Lawson","year":"1979","unstructured":"Lawson, C.L., Hanson, R.J., Kincaid, D.R., Krogh, F.T.: Basic linear algebra subprograms for Fortran usage. ACM Trans. Math. Softw. (TOMS) 5(3), 308\u2013323 (1979)","journal-title":"ACM Trans. Math. Softw. (TOMS)"},{"key":"4_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/978-3-642-19475-7_31","volume-title":"Reconfigurable Computing: Architectures, Tools and Applications","author":"C Lann Le","year":"2011","unstructured":"Le Lann, C., Boland, D., Constantinides, G.: The Krawczyk algorithm: rigorous bounds for linear equation solution on an FPGA. In: Koch, A., Krishnamurthy, R., McAllister, J., Woods, R., El-Ghazawi, T. (eds.) ARC 2011. LNCS, vol. 6578, pp. 287\u2013295. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-19475-7_31"},{"key":"4_CR25","unstructured":"MATLAB: version 7.10.0 (R2010a). The MathWorks Inc., Natick (2010)"},{"key":"4_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"570","DOI":"10.1007\/978-3-642-02658-4_42","volume-title":"Computer Aided Verification","author":"D Monniaux","year":"2009","unstructured":"Monniaux, D.: On using floating-point computations to help an exact linear arithmetic decision procedure. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 570\u2013583. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-02658-4_42"},{"key":"4_CR27","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-8176-4705-6","volume-title":"Handbook of Floating-Point Arithmetic","author":"JM Muller","year":"2009","unstructured":"Muller, J.M., et al.: Handbook of Floating-Point Arithmetic. Springer, Boston (2009). doi: 10.1007\/978-0-8176-4705-6"},{"issue":"2","key":"4_CR28","doi-asserted-by":"crossref","first-page":"283","DOI":"10.1007\/s10107-003-0433-3","volume":"99","author":"A Neumaier","year":"2004","unstructured":"Neumaier, A., Shcherbina, O.: Safe bounds in linear and mixed-integer linear programming. Math. Program. 99(2), 283\u2013296 (2004)","journal-title":"Math. Program."},{"key":"4_CR29","unstructured":"de Oliveira, D.C.B., Monniaux, D.: Experiments on the feasibility of using a floating-point simplex in an SMT solver. In: PAAR@ IJCAR, pp. 19\u201328 (2012)"},{"key":"4_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-319-31769-4_3","volume-title":"Scientific Computing, Computer Arithmetic, and Validated Numerics","author":"J Pryce","year":"2016","unstructured":"Pryce, J.: The forthcoming IEEE standard 1788 for interval arithmetic. In: Nehmeier, M., Wolff von Gudenberg, J., Tucker, W. (eds.) SCAN 2015. LNCS, vol. 9553, pp. 23\u201339. Springer, Cham (2016). doi: 10.1007\/978-3-319-31769-4_3"},{"issue":"1","key":"4_CR31","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1016\/j.jlap.2004.07.008","volume":"64","author":"N Revol","year":"2005","unstructured":"Revol, N., Makino, K., Berz, M.: Taylor models and floating-point arithmetic: proof that arithmetic operations are validated in COSY. J. Logic Algebraic Program. 64(1), 135\u2013154 (2005)","journal-title":"J. Logic Algebraic Program."},{"issue":"1\u20133","key":"4_CR32","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1016\/S0024-3795(00)00279-2","volume":"324","author":"SM Rump","year":"2001","unstructured":"Rump, S.M.: Computational error bounds for multiple or nearly multiple eigenvalues. Linear Algebra Appl. 324(1\u20133), 209\u2013226 (2001)","journal-title":"Linear Algebra Appl."},{"key":"4_CR33","unstructured":"Saad, Y.: Numerical Methods for Large Eigenvalue Problems, vol. 158. SIAM (1992)"},{"key":"4_CR34","unstructured":"Sch\u00e4ling, B.: The Boost C++ Libraries. Boris Sch\u00e4ling (2011)"},{"key":"4_CR35","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511817106","volume-title":"The Cauchy-Schwarz Master Class: An Introduction to the Art of Mathematical Inequalities","author":"JM Steele","year":"2004","unstructured":"Steele, J.M.: The Cauchy-Schwarz Master Class: An Introduction to the Art of Mathematical Inequalities. Cambridge University Press, Cambridge (2004)"},{"key":"4_CR36","volume-title":"Matrix Computations","author":"CF Loan Van","year":"1996","unstructured":"Van Loan, C.F.: Matrix Computations. The Johns Hopkins University Press, Baltimore (1996)"}],"container-title":["Lecture Notes in Computer Science","Numerical Software Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-63501-9_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,29]],"date-time":"2019-09-29T09:51:52Z","timestamp":1569750712000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-63501-9_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319635002","9783319635019"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-63501-9_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}