Muñoz, Cesar A.; Ayala-Rincón, Mauricio; Moscato, Mariano M.; Dutle, Aaron M.; Narkawicz, Anthony J.; Almeida, Ariane Alves; da Silva, Andréia B. Avelar; Ramos, Thiago M. Ferreira Formal verification of termination criteria for first-order recursive functions. (English) Zbl 07800193 J. Autom. Reasoning 67, No. 4, Paper No. 40, 30 p. (2023). MSC: 68V15 PDFBibTeX XMLCite \textit{C. A. Muñoz} et al., J. Autom. Reasoning 67, No. 4, Paper No. 40, 30 p. (2023; Zbl 07800193) Full Text: DOI
Dutle, Aaron; Moscato, Mariano; Titolo, Laura; Muñoz, César; Anderson, Gregory; Bobot, François Formal analysis of the compact position reporting algorithm. (English) Zbl 1458.68273 Formal Asp. Comput. 33, No. 1, 65-86 (2021). MSC: 68U35 65Y04 68P30 68Q60 68W40 PDFBibTeX XMLCite \textit{A. Dutle} et al., Formal Asp. Comput. 33, No. 1, 65--86 (2021; Zbl 1458.68273) Full Text: DOI
Titolo, Laura; Moscato, Mariano M.; Muñoz, César A.; Dutle, Aaron; Bobot, François A formally verified floating-point implementation of the compact position reporting algorithm. (English) Zbl 1460.68128 Havelund, Klaus (ed.) et al., Formal methods. 22nd international symposium, FM 2018, held as part of the federated logic conference, FloC 2018, Oxford, UK, July 15–17, 2018. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10951, 364-381 (2018). MSC: 68U35 65Y04 68P30 68Q60 68W40 PDFBibTeX XMLCite \textit{L. Titolo} et al., Lect. Notes Comput. Sci. 10951, 364--381 (2018; Zbl 1460.68128) Full Text: DOI Link
Rocha, Camilo; Meseguer, José; Muñoz, César Rewriting modulo SMT and open system analysis. (English) Zbl 1353.68156 J. Log. Algebr. Methods Program. 86, No. 1, 269-297 (2017). MSC: 68Q42 68Q60 PDFBibTeX XMLCite \textit{C. Rocha} et al., J. Log. Algebr. Methods Program. 86, No. 1, 269--297 (2017; Zbl 1353.68156) Full Text: DOI
Narkawicz, Anthony; Muñoz, César; Dutle, Aaron Formally-verified decision procedures for univariate polynomial computation based on Sturm’s and Tarski’s theorems. (English) Zbl 1356.68196 J. Autom. Reasoning 54, No. 4, 285-326 (2015). MSC: 68T15 03B35 PDFBibTeX XMLCite \textit{A. Narkawicz} et al., J. Autom. Reasoning 54, No. 4, 285--326 (2015; Zbl 1356.68196) Full Text: DOI
Moscato, Mariano M.; Muñoz, César A.; Smith, Andrew P. Affine arithmetic and applications to real-number proving. (English) Zbl 1465.65042 Urban, Christian (ed.) et al., Interactive theorem proving. 6th international conference, ITP 2015, Nanjing, China, August 24–27, 2015. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9236, 294-309 (2015). MSC: 65G30 65G20 68V20 PDFBibTeX XMLCite \textit{M. M. Moscato} et al., Lect. Notes Comput. Sci. 9236, 294--309 (2015; Zbl 1465.65042) Full Text: DOI
Muñoz, César; Narkawicz, Anthony Formalization of Bernstein polynomials and applications to global optimization. (English) Zbl 1314.68286 J. Autom. Reasoning 51, No. 2, 151-196 (2013). MSC: 68T15 65K10 PDFBibTeX XMLCite \textit{C. Muñoz} and \textit{A. Narkawicz}, J. Autom. Reasoning 51, No. 2, 151--196 (2013; Zbl 1314.68286) Full Text: DOI
Rocha, Camilo; Muñoz, César Simulation and verification of synchronous set relations in rewriting logic. (English) Zbl 1349.68105 Simao, Adenilso (ed.) et al., Formal methods, foundations and applications. 14th Brazilian symposium, SBMF 2011, São Paulo, Brazil, September 26–30, 2011. Revised selected papers. Berlin: Springer (ISBN 978-3-642-25031-6/pbk). Lecture Notes in Computer Science 7021, 60-75 (2011). MSC: 68Q42 03B70 68Q60 PDFBibTeX XMLCite \textit{C. Rocha} and \textit{C. Muñoz}, Lect. Notes Comput. Sci. 7021, 60--75 (2011; Zbl 1349.68105) Full Text: DOI Link
Kirchner, Florent; Muñoz, César The proof monad. (English) Zbl 1208.68144 J. Log. Algebr. Program. 79, No. 3-5, 264-277 (2010). MSC: 68Q55 18C15 68T15 PDFBibTeX XMLCite \textit{F. Kirchner} and \textit{C. Muñoz}, J. Log. Algebr. Program. 79, No. 3--5, 264--277 (2010; Zbl 1208.68144) Full Text: DOI