{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,12]],"date-time":"2026-06-12T04:35:18Z","timestamp":1781238918344,"version":"3.54.1"},"reference-count":42,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2015,2,5]],"date-time":"2015-02-05T00:00:00Z","timestamp":1423094400000},"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":["J Autom Reasoning"],"published-print":{"date-parts":[[2015,4]]},"DOI":"10.1007\/s10817-015-9320-x","type":"journal-article","created":{"date-parts":[[2015,2,4]],"date-time":"2015-02-04T14:18:05Z","timestamp":1423059485000},"page":"285-326","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":17,"title":["Formally-Verified Decision Procedures for Univariate Polynomial Computation Based on Sturm\u2019s and Tarski\u2019s Theorems"],"prefix":"10.1007","volume":"54","author":[{"given":"Anthony","family":"Narkawicz","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"C\u00e9sar","family":"Mu\u00f1oz","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Aaron","family":"Dutle","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2015,2,5]]},"reference":[{"issue":"3","key":"9320_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. J. Autom. Reason. 44(3), 175\u2013205 (2010)","journal-title":"J. Autom. Reason."},{"key":"9320_CR2","unstructured":"Aransay, J., Divas\u00f3n, J.: Formalization and execution of linear algebra: from theorems to algorithms. In: Gupta, G., Pe\u00f1a, R. (eds.) Proceedings, 23rd International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR 2013, Madrid, Spain. Dpto. de Systemas Inform\u00e1ticos y Computation, Universidad Complutense de Madrid, TR-11-13 (2013)"},{"key":"9320_CR3","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-33099-2","volume-title":"Algorithms in Real Algebraic Geometry (Algorithms and Computation in Mathematics)","author":"S Basu","year":"2006","unstructured":"Basu, S., Pollack, R., Roy, M.F.: Algorithms in Real Algebraic Geometry (Algorithms and Computation in Mathematics). Springer-Verlag New York, Inc., USA (2006)"},{"key":"9320_CR4","doi-asserted-by":"crossref","unstructured":"Cohen, C.: Mahboubi, A.: Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination. Logical Methods Comput. Sci. 8(1:02), 1\u201340 (Feb 2012) https:\/\/hal.inria.fr\/inria-00593738","DOI":"10.2168\/LMCS-8(1:2)2012"},{"key":"9320_CR5","first-page":"134","volume-title":"Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In: Second GI Conference on Automata Theory and Formal Languages. Lecture Notes in Computer Science, vol. 33","author":"G Collins","year":"1975","unstructured":"Collins, G.: Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In: Second GI Conference on Automata Theory and Formal Languages. Lecture Notes in Computer Science, vol. 33, pp. 134\u2013183. Springer-Verlag, Kaiserslautern (1975)"},{"key":"9320_CR6","doi-asserted-by":"crossref","unstructured":"Crespo, L.G., Mu\u00f1oz, C.A., Narkawicz, A.J., Kenny, S.P., Giesy, D.P.: Uncertainty analysis via failure domain characterization: Polynomial requirement functions. In.: Proceedings of European Safety and Reliability Conference, p 2011. Troyes, France","DOI":"10.1201\/b11433-162"},{"issue":"2","key":"9320_CR7","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1109\/TC.2008.213","volume":"58","author":"M Daumas","year":"2009","unstructured":"Daumas, M., Lester, D., Mu\u00f1oz, C.: Verified real number calculations: A library for interval arithmetic. IEEE Trans. Comput. 58(2), 1\u201312 (2009)","journal-title":"IEEE Trans. Comput."},{"key":"9320_CR8","doi-asserted-by":"crossref","unstructured":"D\u00e9n\u00e8s, M., M\u00f6rtberg, A., Siles, V.: A refinement-based approach to computational algebra in Coq. In: Beringer, L., Felty, A.P. (eds.) Interactive Theorem Proving - Third International Conference, ITP 2012, Princeton, NJ, USA, August 13-15, 2012. Proceedings. Lecture Notes in Computer Science, vol. 7406, pp. 83\u201398. Springer (2012). doi: 10.1007\/978-3-642-32347-8","DOI":"10.1007\/978-3-642-32347-8"},{"key":"9320_CR9","first-page":"194","volume-title":"Proceedings of the 19th International Symposium on Formal Methods (FM 2014). Lecture Notes in Computer Science, vol. 8442","author":"W Denman","year":"2014","unstructured":"Denman, W., Mu\u00f1oz, C.: Automated real proving in PVS via MetiTarski. In: Jones, C., Pihlajasaari, P., Sun, J (eds.) Proceedings of the 19th International Symposium on Formal Methods (FM 2014). Lecture Notes in Computer Science, vol. 8442, pp. 194\u2013199. Springer, Singapore (2014)"},{"issue":"2","key":"9320_CR10","doi-asserted-by":"crossref","first-page":"242","DOI":"10.1109\/TC.2010.128","volume":"60","author":"F de Dinechin","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":"9320_CR11","unstructured":"Dowek, G., Geser, A., Mu\u00f1oz, C.: Tactical conflict detection and resolution in a 3-D airspace. In: Proceedings of the 4th USA\/Europe Air Traffic Management R&D Seminar, ATM 2001. Santa Fe, New Mexico (2001), a long version appears as report NASA\/CR-2001-210853 ICASE Report No. 2001-7"},{"key":"9320_CR12","doi-asserted-by":"crossref","unstructured":"Eberl, M.: A decision procedure for univariate real polynomials in Isabelle\/HOL. In: Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP \u201915, pp. 75\u201383. ACM, New York (2015). doi: 10.1145\/2676724.2693166","DOI":"10.1145\/2676724.2693166"},{"issue":"9","key":"9320_CR13","doi-asserted-by":"crossref","first-page":"715","DOI":"10.4169\/amer.math.monthly.119.09.715","volume":"119","author":"M Eisermann","year":"2012","unstructured":"Eisermann, M.: The fundamental theorem of algebra made effective: An elementary real-algebraic proof via Sturm chains. Am. Math. Mon. 119(9), 715\u2013752 (2012)","journal-title":"Am. Math. Mon."},{"key":"9320_CR14","doi-asserted-by":"crossref","unstructured":"Gao, S., Kong, S., Clarke, E.M. : dReal: An SMT solver for nonlinear theories over the reals. In: Bonacina, M.P. (ed.) Automated Deduction - CADE-24 - 24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013. Proceedings. Lecture Notes in Computer Science, vol. 7898, pp. 208\u2013214. Springer (2013). doi: 10.1007\/978-3-642-38574-2","DOI":"10.1007\/978-3-642-38574-2"},{"key":"9320_CR15","doi-asserted-by":"crossref","first-page":"303","DOI":"10.1023\/A:1009934614393","volume":"6","author":"J Garloff","year":"2000","unstructured":"Garloff, J.: Application of Bernstein expansion to the solution of control problems. Reliab. Comput. 6, 303\u2013320 (2000)","journal-title":"Reliab. Comput."},{"issue":"1\u20133","key":"9320_CR16","doi-asserted-by":"crossref","first-page":"199","DOI":"10.1016\/S0304-3975(02)00639-4","volume":"297","author":"J von zur Gathen","year":"2003","unstructured":"von zur Gathen, J., L\u00fccking, T.: Subresultants revisited. Theor. Comput. Sci. 297(1\u20133), 199\u2013239 (2003). doi: 10.1016\/S0304-3975(02)00639-4","journal-title":"Theor. Comput. Sci."},{"key":"9320_CR17","first-page":"103","volume-title":"Interactive Theorem Proving - ITP 2011, vol. 6898","author":"G Gonthier","year":"2011","unstructured":"Gonthier, G.: Point-free, set-free concrete linear algebra. In: van Eekelen, M.C.J.D., Geuvers, H., Schmaltz, J., Wiedijk, F (eds.) Interactive Theorem Proving - ITP 2011, vol. 6898, pp. 103\u2013118. Radboud University of Nijmegen, Springer, Berg en Dal, Netherlands (2011). https:\/\/hal.inria.fr\/hal-00805966"},{"issue":"1","key":"9320_CR18","doi-asserted-by":"crossref","first-page":"138","DOI":"10.1145\/1132973.1132980","volume":"32","author":"L Granvilliers","year":"2006","unstructured":"Granvilliers, L., Benhamou, F.: RealPaver: An interval solver using constraint satisfaction techniques. ACM Trans. Math. Softw. 32(1), 138\u2013156 (2006)","journal-title":"ACM Trans. Math. Softw."},{"key":"9320_CR19","volume-title":"Metatheory and reflection in theorem proving: A survey and critique. Technical Report CRC-053","author":"J Harrison","year":"1995","unstructured":"Harrison, J.: Metatheory and reflection in theorem proving: A survey and critique. Technical Report CRC-053. SRI Cambridge, Millers Yard, Cambridge (1995)"},{"key":"9320_CR20","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1007\/BFb0028391","volume-title":"Theorem Proving in Higher Order Logics: 10th International Conference, TPHOLs\u201997. Lecture Notes in Computer Science, vol. 1275","author":"J Harrison","year":"1997","unstructured":"Harrison, J.: Verifying the accuracy of polynomial approximations in HOL. In: Gunter, E.L., Felty, A. (eds.) Theorem Proving in Higher Order Logics: 10th International Conference, TPHOLs\u201997. Lecture Notes in Computer Science, vol. 1275, pp. 137\u2013152. Springer-Verlag, Murray Hill, NJ (1997)"},{"key":"9320_CR21","doi-asserted-by":"crossref","unstructured":"Harrison, J.: Verifying nonlinear real formulas via sums of squares. In: Theorem Proving in Higher Order Logics. Lecture Notes in Computer Science, vol. 4732, pp. 102\u2013118. Springer (2007)","DOI":"10.1007\/978-3-540-74591-4_9"},{"key":"9320_CR22","doi-asserted-by":"crossref","unstructured":"Herencia-Zapana, H., Jobredeaux, R., Owre, S., Garoche, P.L., Feron, E., Perez, G., Ascariz, P.: PVS linear algebra libraries for verification of control software algorithms in C\/ACSL. In: Goodloe, A., Person, S. (eds.) NASA Formal Methods - 4th International Symposium, NFM 2012, Norfolk, VA, USA, April 3-5, 2012. Proceedings. Lecture Notes in Computer Science, vol. 7226, pp. 147\u2013161. Springer (2012). doi: 10.1007\/978-3-642-28891-3","DOI":"10.1007\/978-3-642-28891-3"},{"key":"9320_CR23","volume-title":"Approximate Commutative Algebra","author":"EL Kaltofen","year":"2010","unstructured":"Kaltofen, E.L., Li, B., Yang, Z., Zhi, L.: Exact certification in global polynomial optimization via sums-of-squares of rational functions with rational coefficients. In: Robbiano, L., Abbott, J (eds.) Approximate Commutative Algebra. Springer Vienna, Texts and Monographs in Symbolic Computation (2010)"},{"issue":"4","key":"9320_CR24","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1109\/6979.898217","volume":"1","author":"J Kuchar","year":"2000","unstructured":"Kuchar, J., Yang, L.: A review of conflict detection and resolution modeling methods. IEEE Trans. Intell. Transp. Syst. 1(4), 179\u2013189 (2000)","journal-title":"IEEE Trans. Intell. Transp. Syst."},{"issue":"1","key":"9320_CR25","doi-asserted-by":"crossref","first-page":"99","DOI":"10.1017\/S096012950600586X","volume":"17","author":"A Mahboubi","year":"2007","unstructured":"Mahboubi, A.: Implementing the cylindrical algebraic decomposition within the Coq system. Math. Struct. Comput. Sci. 17(1), 99\u2013127 (2007)","journal-title":"Math. Struct. Comput. Sci."},{"key":"9320_CR26","unstructured":"Mahboubi, A., Pottier, L.: Elimination des quantificateurs sur les r\u00e9els en Coq. In: Journ\u00e9es Francophone des Langages Applicatifs (JFLA) (2002)"},{"key":"9320_CR27","doi-asserted-by":"crossref","unstructured":"Mahmoud, M.Y., Aravantinos, V., Tahar, S.: Formalization of infinite dimension linear spaces with application to quantum theory. In: Brat, G., Rungta, N., Venet, A. (eds.) NASA Formal Methods, 5th International Symposium, NFM 2013, Moffett Field, CA, USA, May 14-16, 2013. Proceedings. Lecture Notes in Computer Science, vol. 7871, pp. 413\u2013427. Springer (2013). doi: 10.1007\/978-3-642-38088-4","DOI":"10.1007\/978-3-642-38088-4"},{"key":"9320_CR28","doi-asserted-by":"crossref","unstructured":"McLaughlin, S., Harrison, J.: A proof-producing decision procedure for real arithmetic. In: Nieuwenhuis, R. (ed.) Proceedings of the 20th International Conference on Automated Deduction, proceedings. Lecture Notes in Computer Science, vol. 3632, pp. 295\u2013314 (2005)","DOI":"10.1007\/11532231_22"},{"key":"9320_CR29","unstructured":"Melquiond, G.: Proving bounds on real-valued functions with computations. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12-15, 2008, Proceedings. Lecture Notes in Computer Science, vol. 5195, pp. 2\u201317. Springer (2008). 10.1007\/978-3-540-71070-7_2"},{"key":"9320_CR30","doi-asserted-by":"crossref","unstructured":"Monniaux, D., Corbineau, P.: On the generation of Positivstellensatz witnesses in degenerate cases. In: Proceedings of Interactive Theorem Proving (ITP). Lecture Notes in Computer Science (2011)","DOI":"10.1007\/978-3-642-22863-6_19"},{"key":"9320_CR31","unstructured":"de Moura, L., Passmore, G.: Computation in real closed infinitesimal and transcendental extensions of the rationals. In: Automated Deduction - CADE-24, 24th International Conference on Automated Deduction, Lake Placid, New York, June 9-14, 2013, Proceedings (2013)"},{"key":"9320_CR32","unstructured":"Mu\u00f1oz, C.: Rapid prototyping in PVS. Contractor Report NASA\/CR-2003-212418, NASA, Langley Research Center, Hampton VA 23681-2199, USA (2003)"},{"issue":"2","key":"9320_CR33","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1007\/s10817-012-9256-3","volume":"51","author":"C Mu\u00f1oz","year":"2013","unstructured":"Mu\u00f1oz, C., Narkawicz, A.: Formalization of a representation of Bernstein polynomials and applications to global optimization. J. Autom. Reason. 51(2), 151\u2013196 (2013). doi: 10.1007\/s10817-012-9256-3","journal-title":"J. Autom. Reason."},{"key":"9320_CR34","doi-asserted-by":"crossref","unstructured":"Narkawicz, A., Mu\u00f1oz, C.: A formally verified generic branching algorithm for global optimization. In: Cohen, E., Rybalchenko, A. (eds.) Fifth Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE 2013). Lecture Notes in Computer Science, vol. 8164, pp. 326\u2013343. Springer (2014)","DOI":"10.1007\/978-3-642-54108-7_17"},{"key":"9320_CR35","unstructured":"Narkawicz, A.J., Mu\u00f1oz, C.A.: A formally-verified decision procedure for univariate polynomial computation based on Sturm\u2019s theorem. Technical Memorandum NASA\/TM-2014-218548, NASA, Langley Research Center, Hampton VA 23681-2199, USA (2014)"},{"key":"9320_CR36","doi-asserted-by":"crossref","unstructured":"Owre, S., Rushby, J., Shankar, N.: PVS: A prototype verification system. In: Kapur, D. (ed.) Proceeding of the 11th International Conference on Automated Deduction (CADE). Lecture Notes in Artificial Intelligence, vol. 607, pp. 748\u2013752. Springer (1992)","DOI":"10.1007\/3-540-55602-8_217"},{"key":"9320_CR37","doi-asserted-by":"crossref","unstructured":"Passmore, G.O., Jackson, P.B.: Combined decision techniques for the existential theory of the reals. In: Dixon, L. (ed.) Proceedings of Calculemus\/Mathematical Knowledge Management. pp. 122\u2013137. No. 5625 in LNAI. Springer-Verlag (2009)","DOI":"10.1007\/978-3-642-02614-0_14"},{"key":"9320_CR38","volume-title":"Efficiently executing PVS. Tech. rep., Project Report, ComputerScience Laboratory","author":"N Shankar","year":"1999","unstructured":"Shankar, N.: Efficiently executing PVS. Tech. rep., Project Report, ComputerScience Laboratory. SRI International, Menlo Park (1999)"},{"key":"9320_CR39","doi-asserted-by":"crossref","unstructured":"Solovyev, A., Hales, T.C.: Formal verification of nonlinear inequalities with Taylor interval approximations. In: Brat, G., Rungta, N., Venet, A. (eds.) Proceedings of the 5th International Symposium NASA Formal Methods. Lecture Notes in Computer Science, vol. 7871, pp. 383\u2013397 (2013)","DOI":"10.1007\/978-3-642-38088-4_26"},{"key":"9320_CR40","unstructured":"Sottile, F.: Chapter 2: Real solutions to univariate polynomials. course Notes. http:\/\/www.math.tamu.edu\/sottile\/teaching\/10.S\/Ch2.pdf"},{"key":"9320_CR41","doi-asserted-by":"crossref","unstructured":"Sturm, C.: M\u00e9moire sur la r\u00e9solution des \u00e9quations num\u00e9riques. In: Pont, J.C. (ed.) Collected Works of Charles Fran\u00e7ois Sturm, pp. 345\u2013390. Birkh\u00e4user Basel (2009). doi: 10.1007\/978-3-7643-7990-2_29","DOI":"10.1007\/978-3-7643-7990-2_29"},{"key":"9320_CR42","doi-asserted-by":"crossref","unstructured":"Tarski, A.: A decision method for elementary algebra and geometry. Bull. Am. Math. Soc., 59 (1951)","DOI":"10.1525\/9780520348097"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-015-9320-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-015-9320-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-015-9320-x","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,4,28]],"date-time":"2022-04-28T14:35:41Z","timestamp":1651156541000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-015-9320-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,2,5]]},"references-count":42,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2015,4]]}},"alternative-id":["9320"],"URL":"https:\/\/doi.org\/10.1007\/s10817-015-9320-x","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,2,5]]}}}