{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T17:36:15Z","timestamp":1725903375788},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319630458"},{"type":"electronic","value":"9783319630465"}],"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-63046-5_7","type":"book-chapter","created":{"date-parts":[[2017,7,10]],"date-time":"2017-07-10T13:34:07Z","timestamp":1499693647000},"page":"95-113","source":"Crossref","is-referenced-by-count":8,"title":["Satisfiability Modulo Transcendental Functions via Incremental Linearization"],"prefix":"10.1007","author":[{"given":"Alessandro","family":"Cimatti","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alberto","family":"Griggio","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ahmed","family":"Irfan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marco","family":"Roveri","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Roberto","family":"Sebastiani","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,7,11]]},"reference":[{"issue":"3","key":"7_CR1","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1007\/s10817-009-9149-2","volume":"44","author":"B Akbarpour","year":"2010","unstructured":"Akbarpour, B., Paulson, L.C.: MetiTarski: an automatic theorem prover for real-valued special functions. JAR 44(3), 175\u2013205 (2010)","journal-title":"JAR"},{"doi-asserted-by":"crossref","unstructured":"Allamigeon, X., Gaubert, S., Magron, V., Werner, B.: Certification of inequalities involving transcendental functions: combining SDP and max-plus approximation. In: 2013 European Control Conference (ECC), pp. 2244\u20132250. IEEE (2013)","key":"7_CR2","DOI":"10.23919\/ECC.2013.6669514"},{"doi-asserted-by":"crossref","unstructured":"Bak, S., Bogomolov, S., Johnson, T.T.: HYST: a source transformation and translation tool for hybrid automaton models. In: Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, pp. 128\u2013133. ACM (2015)","key":"7_CR3","DOI":"10.1145\/2728606.2728630"},{"key":"7_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1007\/978-3-319-08867-9_22","volume-title":"Computer Aided Verification","author":"R Cavada","year":"2014","unstructured":"Cavada, R., Cimatti, A., Dorigatti, M., Griggio, A., Mariotti, A., Micheli, A., Mover, S., Roveri, M., Tonetta, S.: The nuXmv symbolic model checker. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 334\u2013342. Springer, Cham (2014). doi: 10.1007\/978-3-319-08867-9_22"},{"doi-asserted-by":"crossref","unstructured":"Cimatti, A., Griggio, A., Irfan, A., Roveri, M., Sebastiani, R.: Invariant checking of NRA transition systems via incremental reduction to LRA with EUF. In: Legay and Margaria [16], pp. 58\u201375. https:\/\/es-static.fbk.eu\/people\/griggio\/papers\/tacas17.pdf","key":"7_CR5","DOI":"10.1007\/978-3-662-54577-5_4"},{"key":"7_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/978-3-662-46681-0_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Cimatti","year":"2015","unstructured":"Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: HyComp: an SMT-Based model checker for hybrid systems. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 52\u201367. Springer, Heidelberg (2015). doi: 10.1007\/978-3-662-46681-0_4"},{"key":"7_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-642-36742-7_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Cimatti","year":"2013","unstructured":"Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT solver. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 93\u2013107. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-36742-7_7"},{"key":"7_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1007\/978-3-319-48989-6_11","volume-title":"FM 2016: Formal Methods","author":"A Cimatti","year":"2016","unstructured":"Cimatti, A., Mover, S., Sessa, M.: From electrical switched networks to hybrid automata. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds.) FM 2016. LNCS, vol. 9995, pp. 164\u2013181. Springer, Cham (2016). doi: 10.1007\/978-3-319-48989-6_11"},{"issue":"2","key":"7_CR9","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., 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":"7_CR10","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/978-3-642-24364-6_9","volume-title":"Frontiers of Combining Systems","author":"A Eggers","year":"2011","unstructured":"Eggers, A., Kruglov, E., Kupferschmid, S., Scheibler, K., Teige, T., Weidenbach, C.: Superposition modulo non-linear arithmetic. In: Tinelli, C., Sofronie-Stokkermans, V. (eds.) FroCoS 2011. LNCS (LNAI), vol. 6989, pp. 119\u2013134. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-24364-6_9"},{"issue":"3\u20134","key":"7_CR11","first-page":"209","volume":"1","author":"M Fr\u00e4nzle","year":"2007","unstructured":"Fr\u00e4nzle, M., Herde, C., Teige, T., Ratschan, S., Schubert, T.: Efficient solving of large non-linear arithmetic constraint systems with complex boolean structure. JSAT 1(3\u20134), 209\u2013236 (2007)","journal-title":"JSAT"},{"key":"7_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"286","DOI":"10.1007\/978-3-642-31365-3_23","volume-title":"Automated Reasoning","author":"S Gao","year":"2012","unstructured":"Gao, S., Avigad, J., Clarke, E.M.: $$\\delta $$ -Complete decision procedures for satisfiability over the reals. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 286\u2013300. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-31365-3_23"},{"key":"7_CR13","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/978-3-642-38574-2_14","volume-title":"Automated Deduction \u2013 CADE-24","author":"S Gao","year":"2013","unstructured":"Gao, S., Kong, S., Clarke, E.M.: dReal: An SMT solver for nonlinear theories over the reals. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 208\u2013214. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-38574-2_14"},{"unstructured":"Gario, M., Micheli, A.: PySMT: a solver-agnostic library for fast prototyping of SMT-based algorithms. In: SMT, pp. 373\u2013384 (2015)","key":"7_CR14"},{"unstructured":"Hazewinkel, M.: Encyclopaedia of Mathematics: Stochastic Approximation Zygmund Class of Functions. Encyclopaedia of Mathematics. Springer, Netherlands (1993). https:\/\/books.google.it\/books?id=1ttmCRCerVUC","key":"7_CR15"},{"key":"7_CR16","series-title":"Lecture Notes in Computer Science","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","year":"2017","unstructured":"Legay, A., Margaria, T. (eds.): TACAS 2017. LNCS, vol. 10205. Springer, Heidelberg (2017)"},{"key":"7_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1007\/978-3-662-44199-2_49","volume-title":"Mathematical Software \u2013 ICMS 2014","author":"V Magron","year":"2014","unstructured":"Magron, V.: NLCertify: a tool for formal nonlinear optimization. In: Hong, H., Yap, C. (eds.) ICMS 2014. LNCS, vol. 8592, pp. 315\u2013320. Springer, Heidelberg (2014). doi: 10.1007\/978-3-662-44199-2_49"},{"issue":"3","key":"7_CR18","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1007\/s10817-015-9350-4","volume":"57","author":"\u00c9 Martin-Dorel","year":"2016","unstructured":"Martin-Dorel, \u00c9., Melquiond, G.: Proving tight bounds on univariate expressions with elementary functions in Coq. J. Autom. Reasoning 57(3), 187\u2013217 (2016)","journal-title":"J. Autom. Reasoning"},{"unstructured":"Melquiond, G.: Coq-interval (2011)","key":"7_CR19"},{"key":"7_CR20","doi-asserted-by":"crossref","DOI":"10.1002\/9781118627372","volume-title":"Integer and Combinatorial Optimization","author":"GL Nemhauser","year":"1988","unstructured":"Nemhauser, G.L., Wolsey, L.A.: Integer and Combinatorial Optimization. Wiley-Interscience, New York (1988)"},{"unstructured":"Nieven, I.: Numbers: Rational and Irrational. Mathematical Association of America (1961)","key":"7_CR21"},{"issue":"4","key":"7_CR22","doi-asserted-by":"crossref","first-page":"723","DOI":"10.1145\/1183278.1183282","volume":"7","author":"S Ratschan","year":"2006","unstructured":"Ratschan, S.: Efficient solving of quantified inequality constraints over the real numbers. TOCL 7(4), 723\u2013748 (2006)","journal-title":"TOCL"},{"doi-asserted-by":"crossref","unstructured":"Roohi, N., Prabhakar, P., Viswanathan, M.: HARE: A hybrid abstraction refinement engine for verifying non-linear hybrid automata. In: Legay and Margaria [16], pp. 573\u2013588","key":"7_CR23","DOI":"10.1007\/978-3-662-54577-5_33"},{"key":"7_CR24","first-page":"231","volume":"13","author":"K Scheibler","year":"2013","unstructured":"Scheibler, K., Kupferschmid, S., Becker, B.: Recent improvements in the SMT solver iSAT. MBMV 13, 231\u2013241 (2013)","journal-title":"MBMV"},{"key":"7_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1007\/978-3-642-38088-4_26","volume-title":"NASA Formal Methods","author":"A Solovyev","year":"2013","unstructured":"Solovyev, A., Hales, T.C.: Formal verification of nonlinear inequalities with taylor interval approximations. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol. 7871, pp. 383\u2013397. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-38088-4_26"},{"unstructured":"Townsend, E.: Functions of a Complex Variable. Read Books (2007)","key":"7_CR26"},{"key":"7_CR27","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/978-3-642-02959-2_10","volume-title":"Automated Deduction \u2013 CADE-22","author":"C Weidenbach","year":"2009","unstructured":"Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: SPASS version 3.5. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol. 5663, pp. 140\u2013145. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-02959-2_10"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 26"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-63046-5_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,6,25]],"date-time":"2024-06-25T10:13:43Z","timestamp":1719310423000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-63046-5_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319630458","9783319630465"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-63046-5_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}