Mariano M. Moscato

33 papers A 2B 10C 4Journal 6Unranked 9
YearRankTypeTitle / Venue / Authors
2025 C conf
A PVS Library on the Infinitude of Primes.
CICM
Bruno Berto de Oliveira Ribeiro, Mariano M. Moscato, Thaynara Arielly de Lima, Mauricio Ayala-Rincón
2025 — conf
Verification of an Anti-unification Algorithm in PVS.
NFM
Mauricio Ayala-Rincón, Thaynara Arielly de Lima, Maria Júlia Dias Lima, Mariano M. Moscato, Temur Kutsia
2024 — conf
Rigorous Floating-Point Round-Off Error Analysis in PRECiSA 4.0.
FM (2)
Laura Titolo, Mariano M. Moscato, Marco A. Feliú, Paolo Masci, César A. Muñoz
2023 B conf
A Provably Correct Floating-Point Implementation of Well Clear Avionics Concepts.
FMCAD
Nikson Bernardes Fernandes Ferreira, Mariano M. Moscato, Laura Titolo, Mauricio Ayala-Rincón
2023 — conf
Embedding Differential Dynamic Logic in PVS.
LSFA/HCVS
J. Tanner Slagel, Mariano M. Moscato, Lauren M. White, César A. Muñoz, Swee Balachandran, Aaron Dutle
2023 — ch.
Floating-Point Round-off Error Analysis of Safety-Critical Avionics Software.
Challenges of Software Verification
Laura Titolo, Mariano M. Moscato, Marco A. Feliú, Aaron Dutle, César A. Muñoz
2023 J jnl
Formal Verification of Termination Criteria for First-Order Recursive Functions.
J. Autom. Reason.
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
2023 J jnl
Selected extended papers of NFM 2021.
Innov. Syst. Softw. Eng.
Aaron Dutle, Mariano M. Moscato, Laura Titolo, César A. Muñoz, Ivan Perez
2022 — conf
Interpretation and Formalization of the Right-of-Way Rules.
FACS
Victor A. Carreño, Mariano M. Moscato, Paolo M. Masci, Aaron Dutle
2022 — conf
Towards an implementation of differential dynamic logic in PVS.
SOAP@PLDI
J. Tanner Slagel, César A. Muñoz, Swee Balachandran, Mariano M. Moscato, Aaron Dutle, Paolo Masci, Lauren M. White
2021 B conf
Formal Verification of Termination Criteria for First-Order Recursive Functions.
ITP
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
2021 J jnl
Formal analysis of the compact position reporting algorithm.
Formal Aspects Comput.
Aaron Dutle, Mariano M. Moscato, Laura Titolo, César A. Muñoz, Gregory Anderson, François Bobot
2021 — ed.
NASA Formal Methods - 13th International Symposium, NFM 2021, Virtual Event, May 24-28, 2021, Proceedings
NFM
Aaron Dutle, Mariano M. Moscato, Laura Titolo, César A. Muñoz, Ivan Perez
2020 B conf
Automatic Generation of Guard-Stable Floating-Point Code.
IFM
Laura Titolo, Mariano M. Moscato, Marco A. Feliú, César A. Muñoz
2020 J jnl
Automatic generation and verification of test-stable floating-point code.
CoRR
Laura Titolo, Mariano M. Moscato, César A. Muñoz
2019 — conf
A Mixed Real and Floating-Point Solver.
NFM
Rocco Salvia, Laura Titolo, Marco A. Feliú, Mariano M. Moscato, César A. Muñoz, Zvonimir Rakamaric
2019 B conf
Provably Correct Floating-Point Implementation of a Point-in-Polygon Algorithm.
FM
Mariano M. Moscato, Laura Titolo, Marco A. Feliú, César A. Muñoz
2018 B conf
A Formally Verified Floating-Point Implementation of the Compact Position Reporting Algorithm.
FM
Laura Titolo, Mariano M. Moscato, César A. Muñoz, Aaron Dutle, François Bobot
2018 B conf
An Abstract Interpretation Framework for the Round-Off Error Analysis of Floating-Point Programs.
VMCAI
Laura Titolo, Marco A. Feliú, Mariano M. Moscato, César A. Muñoz
2018 B conf
Boosting the Reuse of Formal Specifications.
ITP
Mariano M. Moscato, Carlos Gustavo López Pombo, César A. Muñoz, Marco A. Feliú
2018 C conf
Eliminating Unstable Tests in Floating-Point Programs.
LOPSTR
Laura Titolo, César A. Muñoz, Marco A. Feliú, Mariano M. Moscato
2018 J jnl
Eliminating Unstable Tests in Floating-Point Programs.
CoRR
Laura Titolo, César A. Muñoz, Marco A. Feliú, Mariano M. Moscato
2018 C conf
Formalization of the Undecidability of the Halting Problem for a Functional Language.
WoLLIC
Thiago Mendonça Ferreira Ramos, César A. Muñoz, Mauricio Ayala-Rincón, Mariano M. Moscato, Aaron Dutle, Anthony Narkawicz
2018 — conf
Towards a Formal Safety Framework for Trajectories.
NFM
Marco A. Feliú, Mariano M. Moscato
2017 — conf
A Formal Analysis of the Compact Position Reporting Algorithm.
VSTTE
Aaron Dutle, Mariano M. Moscato, Laura Titolo, César A. Muñoz
2017 B conf
Automatic Estimation of Verified Floating-Point Round-Off Errors via Static Analysis.
SAFECOMP
Mariano M. Moscato, Laura Titolo, Aaron Dutle, César A. Muñoz
2015 B conf
Affine Arithmetic and Applications to Real-Number Proving.
ITP
Mariano M. Moscato, César A. Muñoz, Andrew P. Smith
2014 J jnl
Dynamite: A tool for the verification of alloy models based on PVS.
ACM Trans. Softw. Eng. Methodol.
Mariano M. Moscato, Carlos López Pombo, Marcelo F. Frias
2013 — conf
HeteroGenius: A Framework for Hybrid Analysis of Heterogeneous Software Specifications.
LAFM
Manuel Giménez, Mariano M. Moscato, Carlos Gustavo López Pombo, Marcelo F. Frias
2013 A conf
Improving Test Generation under Rich Contracts by Tight Bounds and Incremental SAT Solving.
ICST
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
2010 C conf
Dynamite 2.0: New Features Based on UnSAT-Core Extraction to Improve Verification of Software Requirements.
ICTAC
Mariano M. Moscato, Carlos López Pombo, Marcelo F. Frias
2009 B conf
Describing and Analyzing Behaviours over Tabular Specifications Using (Dyn)Alloy.
FASE
Nazareno Aguirre, Marcelo F. Frias, Mariano M. Moscato, T. S. E. Maibaum, Alan Wassyng
2007 A conf
Alloy Analyzer+PVS in the Analysis and Verification of Alloy Specifications.
TACAS
Marcelo F. Frias, Carlos López Pombo, Mariano M. Moscato