Alloy Analyzer+PVS in the Analysis and Verification of Alloy Specifications. - Marcelo F. Frias; Carlos López Pombo; Mariano M. Moscato (TACAS, 2007)

Describing and Analyzing Behaviours over Tabular Specifications Using (Dyn)Alloy. - Nazareno Aguirre; Marcelo F. Frias; Mariano M. Moscato; T. S. E. Maibaum; Alan Wassyng (FASE, 2009)

Dynamite 2.0: New Features Based on UnSAT-Core Extraction to Improve Verification of Software Requirements. - Mariano M. Moscato; Carlos López Pombo; Marcelo F. Frias (ICTAC, 2010)

Improving Test Generation under Rich Contracts by Tight Bounds and Incremental SAT Solving. - 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 (ICST, 2013)

HeteroGenius: A Framework for Hybrid Analysis of Heterogeneous Software Specifications. - Manuel Giménez; Mariano M. Moscato; Carlos Gustavo López Pombo; Marcelo F. Frias (LAFM, 2013)

Dynamite: A tool for the verification of alloy models based on PVS. - Mariano M. Moscato; Carlos López Pombo; Marcelo F. Frias (ACM Trans. Softw. Eng. Methodol., 2014)

Affine Arithmetic and Applications to Real-Number Proving. - Mariano M. Moscato; César A. Muñoz; Andrew P. Smith 001 (ITP, 2015)

Automatic Estimation of Verified Floating-Point Round-Off Errors via Static Analysis. - Mariano M. Moscato; Laura Titolo; Aaron Dutle; César A. Muñoz (SAFECOMP, 2017)

A Formal Analysis of the Compact Position Reporting Algorithm. - Aaron Dutle; Mariano M. Moscato; Laura Titolo; César A. Muñoz (VSTTE, 2017)

A Formally Verified Floating-Point Implementation of the Compact Position Reporting Algorithm. - Laura Titolo; Mariano M. Moscato; César A. Muñoz; Aaron Dutle; François Bobot (FM, 2018)

Boosting the Reuse of Formal Specifications. - Mariano M. Moscato; Carlos Gustavo López Pombo; César A. Muñoz; Marco A. Feliú (ITP, 2018)

Eliminating Unstable Tests in Floating-Point Programs. - Laura Titolo; César A. Muñoz; Marco A. Feliú; Mariano M. Moscato (LOPSTR, 2018)

Towards a Formal Safety Framework for Trajectories. - Marco A. Feliú; Mariano M. Moscato (NFM, 2018)

An Abstract Interpretation Framework for the Round-Off Error Analysis of Floating-Point Programs. - Laura Titolo; Marco A. Feliú; Mariano M. Moscato; César A. Muñoz (VMCAI, 2018)

Formalization of the Undecidability of the Halting Problem for a Functional Language. - Thiago Mendonça Ferreira Ramos; César A. Muñoz; Mauricio Ayala-Rincón; Mariano M. Moscato; Aaron Dutle; Anthony Narkawicz (WoLLIC, 2018)

Provably Correct Floating-Point Implementation of a Point-in-Polygon Algorithm. - Mariano M. Moscato; Laura Titolo; Marco A. Feliú; César A. Muñoz (FM, 2019)

A Mixed Real and Floating-Point Solver. - Rocco Salvia; Laura Titolo; Marco A. Feliú; Mariano M. Moscato; César A. Muñoz; Zvonimir Rakamaric (NFM, 2019)

Automatic Generation of Guard-Stable Floating-Point Code. - Laura Titolo; Mariano M. Moscato; Marco A. Feliú; César A. Muñoz (IFM, 2020)

Automatic generation and verification of test-stable floating-point code. - Laura Titolo; Mariano M. Moscato; César A. Muñoz (CoRR, 2020)

Formal analysis of the compact position reporting algorithm. - Aaron Dutle; Mariano M. Moscato; Laura Titolo; César A. Muñoz; Gregory Anderson 003; François Bobot (Formal Aspects Comput., 2021)

Interpretation and Formalization of the Right-of-Way Rules. - Victor A. Carreño; Mariano M. Moscato; Paolo M. Masci; Aaron Dutle (FACS, 2022)

Towards an implementation of differential dynamic logic in PVS. - J. Tanner Slagel; César A. Muñoz; Swee Balachandran; Mariano M. Moscato; Aaron Dutle; Paolo Masci 001; Lauren M. White (SOAP@PLDI, 2022)

A Provably Correct Floating-Point Implementation of Well Clear Avionics Concepts. - Nikson Bernardes Fernandes Ferreira; Mariano M. Moscato; Laura Titolo; Mauricio Ayala-Rincón (FMCAD, 2023)

Embedding Differential Dynamic Logic in PVS. - J. Tanner Slagel; Mariano M. Moscato; Lauren M. White; César A. Muñoz; Swee Balachandran; Aaron Dutle (LSFA/HCVS, 2023)

Floating-Point Round-off Error Analysis of Safety-Critical Avionics Software. - Laura Titolo; Mariano M. Moscato; Marco A. Feliú; Aaron Dutle; César A. Muñoz (Challenges of Software Verification, 2023)

Selected extended papers of NFM 2021. - Aaron Dutle; Mariano M. Moscato; Laura Titolo; César A. Muñoz; Ivan Perez 001 (Innov. Syst. Softw. Eng., 2023)

Formal Verification of Termination Criteria for First-Order Recursive Functions. - 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 (J. Autom. Reason., 2023)

Rigorous Floating-Point Round-Off Error Analysis in PRECiSA 4.0. - Laura Titolo; Mariano M. Moscato; Marco A. Feliú; Paolo Masci 001; César A. Muñoz (FM (2), 2024)

Verification of an Anti-unification Algorithm in PVS. - Mauricio Ayala-Rincón; Thaynara Arielly de Lima; Maria Júlia Dias Lima; Mariano M. Moscato; Temur Kutsia (NFM, 2025)