Mariano M. Moscato

Publication Activity (10 Years)

Years Active: 2007-2024
Publications (10 Years): 22

Top Topics

Provably Correct

Formal Analysis

Recursive Functions

Top Venues

Publications

J. Tanner Slagel, Mariano M. Moscato, Lauren M. White, César A. Muñoz, Swee Balachandran, Aaron Dutle
Embedding Differential Dynamic Logic in PVS. CoRR (2024)
Aaron Dutle, Mariano M. Moscato, Laura Titolo, César A. Muñoz, Ivan Perez
Selected extended papers of NFM 2021. Innov. Syst. Softw. Eng. 19 (4) (2023)
Nikson Bernardes Fernandes Ferreira, Mariano M. Moscato, Laura Titolo, Mauricio Ayala-Rincón
A Provably Correct Floating-Point Implementation of Well Clear Avionics Concepts. FMCAD (2023)
César A. Muñoz, Mauricio Ayala-Rincón, Mariano M. Moscato, Aaron Dutle, Anthony J. Narkawicz, Ariane Alves Almeida, Andréia B. Avelar da Silva, Thiago Mendonça Ferreira Ramos
Formal Verification of Termination Criteria for First-Order Recursive Functions. J. Autom. Reason. 67 (4) (2023)
Victor A. Carreño, Mariano M. Moscato, Paolo M. Masci, Aaron Dutle
Interpretation and Formalization of the Right-of-Way Rules. FACS (2022)
J. Tanner Slagel, César Muñoz, Swee Balachandran, Mariano M. Moscato, Aaron Dutle, Paolo Masci, Lauren White
Towards an implementation of differential dynamic logic in PVS. SOAP@PLDI (2022)
Aaron Dutle, Mariano M. Moscato, Laura Titolo, César A. Muñoz, Gregory Anderson, François Bobot
Formal analysis of the compact position reporting algorithm. Formal Aspects Comput. 33 (1) (2021)
César A. Muñoz, Mauricio Ayala-Rincón, Mariano M. Moscato, Aaron Dutle, Anthony J. Narkawicz, Ariane Alves Almeida, Andréia B. Avelar, Thiago Mendonça Ferreira Ramos
Formal Verification of Termination Criteria for First-Order Recursive Functions. ITP (2021)
Laura Titolo, Mariano M. Moscato, César A. Muñoz
Automatic generation and verification of test-stable floating-point code. CoRR (2020)
Laura Titolo, Mariano M. Moscato, Marco A. Feliú, César A. Muñoz
Automatic Generation of Guard-Stable Floating-Point Code. IFM (2020)
Mariano M. Moscato, Laura Titolo, Marco A. Feliú, César A. Muñoz
Provably Correct Floating-Point Implementation of a Point-in-Polygon Algorithm. FM (2019)
Rocco Salvia, Laura Titolo, Marco A. Feliú, Mariano M. Moscato, César A. Muñoz, Zvonimir Rakamaric
A Mixed Real and Floating-Point Solver. NFM (2019)
Thiago Mendonça Ferreira Ramos, César A. Muñoz, Mauricio Ayala-Rincón, Mariano M. Moscato, Aaron Dutle, Anthony Narkawicz
Formalization of the Undecidability of the Halting Problem for a Functional Language. WoLLIC (2018)
Marco A. Feliú, Mariano M. Moscato
Towards a Formal Safety Framework for Trajectories. NFM (2018)
Laura Titolo, Mariano M. Moscato, César A. Muñoz, Aaron Dutle, François Bobot
A Formally Verified Floating-Point Implementation of the Compact Position Reporting Algorithm. FM (2018)
Laura Titolo, César A. Muñoz, Marco A. Feliú, Mariano M. Moscato
Eliminating Unstable Tests in Floating-Point Programs. CoRR (2018)
Mariano M. Moscato, Carlos Gustavo López Pombo, César A. Muñoz, Marco A. Feliú
Boosting the Reuse of Formal Specifications. ITP (2018)
Laura Titolo, César A. Muñoz, Marco A. Feliú, Mariano M. Moscato
Eliminating Unstable Tests in Floating-Point Programs. LOPSTR (2018)
Laura Titolo, Marco A. Feliú, Mariano M. Moscato, César A. Muñoz
An Abstract Interpretation Framework for the Round-Off Error Analysis of Floating-Point Programs. VMCAI (2018)
Aaron Dutle, Mariano M. Moscato, Laura Titolo, César A. Muñoz
A Formal Analysis of the Compact Position Reporting Algorithm. VSTTE (2017)
Mariano M. Moscato, Laura Titolo, Aaron Dutle, César A. Muñoz
Automatic Estimation of Verified Floating-Point Round-Off Errors via Static Analysis. SAFECOMP (2017)
Mariano M. Moscato, César A. Muñoz, Andrew P. Smith
Affine Arithmetic and Applications to Real-Number Proving. ITP (2015)
Mariano M. Moscato, Carlos López Pombo, Marcelo F. Frias
Dynamite: A tool for the verification of alloy models based on PVS. ACM Trans. Softw. Eng. Methodol. 23 (2) (2014)
Pablo Abad, Nazareno Aguirre, Valeria S. Bengolea, Daniel Alfredo Ciolek, Marcelo F. Frias, Juan P. Galeotti, Tom Maibaum, Mariano M. Moscato, Nicolás Rosner, Ignacio Vissani
Improving Test Generation under Rich Contracts by Tight Bounds and Incremental SAT Solving. ICST (2013)
Manuel Giménez, Mariano M. Moscato, Carlos Gustavo López Pombo, Marcelo F. Frias
HeteroGenius: A Framework for Hybrid Analysis of Heterogeneous Software Specifications. LAFM (2013)
Mariano M. Moscato, Carlos López Pombo, Marcelo F. Frias
Dynamite 2.0: New Features Based on UnSAT-Core Extraction to Improve Verification of Software Requirements. ICTAC (2010)
Nazareno Aguirre, Marcelo F. Frias, Mariano M. Moscato, T. S. E. Maibaum, Alan Wassyng
Describing and Analyzing Behaviours over Tabular Specifications Using (Dyn)Alloy. FASE (2009)
Marcelo F. Frias, Carlos López Pombo, Mariano M. Moscato
Alloy Analyzer+PVS in the Analysis and Verification of Alloy Specifications. TACAS (2007)