Mariano Moscato

Mariano Moscato

Research Scientist

Tel: +1 (757) 325-6904

Email: mariano.moscato@nianet.org

Mariano Moscato

Education

  • Ph.D., University of Buenos Aires, 2014
  • M.Sc. (C.S.), University of Buenos Aires, 2005
  • B.Sc. (C.S.), University of Buenos Aires, 2003

Work Experience

  • Research Scientist II, National Institute of Aerospace, 2017-present 
  • Research Scientist I, National Institute of Aerospace, 2015-2016
  • Postdoctoral Research Scholar, National Institute of Aerospace, 2014-2016
  • Outreach Secretary, C.S. Dpt., School of Science, University of Buenos Aires, 2012-2014
  • Head Teaching Assistant, University of Buenos Aires, 2010-2014
  • Software Engineer Jr., Axxon, 2003-2005

Research Areas/Expertise

  • Formal Methods in Software Engineering
  • Interactive Theorem Proving
  • Integration of Formal Analysis Techniques
  • Floating-Point Arithmetic
  • Formal Analysis of Safety-Critical Systems
  • Theory of Computation

Current Research

Formal Analysis of Floating-Point Calculations  

Round-off errors in floating-point computations can lead to catastrophic consequences when occurring in safety-critical systems. For this reason, it is crucial to develop formal methods to ensure that the behavior of the implementation of numerical calculations respects properties of interest with respect to the ideal real-number description. A contribution to this field is the development of a fully automatic tool (PRECiSA, http://precisa.nianet.org), aimed to the estimation of round-off errors of floating-point programs. PRECiSA takes as input a program and calculates a bound for the roundoff error of the outcome given by every possible control flow of the program. When provided with ranges for the parameters of the program, PRECiSA also calculates concrete numerical bounds for the roundoff error of the program. Additionally, it automatically generates formal proofs of the correctness of both the generic and numerical bounds. 

Improvement of the Reliability of Floating-Point Programs  

The correctness of a floating-point program is usually analyzed by relating its result with the expected outcome given by an ideal algorithm on real numbers. Significative round-off errors arising in the expressions used in the guard of a conditional statement may cause the control flow of a floating-point program to deviate from its real-valued counterpart. In the context of this project, a novel formal technique based on program transformation has been developed. Its primary goal is to automatically detect and correct programs in which such problems could occur. This technique transforms a floating-point program into a new one that returns the same result than the original for every possible input that causes no flow divergence and a warning for arguments that could provoke it. The technique is being applied to geofencing algorithms implemented in C.

Termination Analysis and Applications 

Most dependable software components of critical systems are expected to perform calculations on given inputs and to provide feedback after a limited amount of time. Strict bounds on the time of response of such systems are usually stated to assure the safety of their execution. Then, the problem of determining whether a program terminates or not for a given input is one of the fundamental areas of research in the field of formal analysis of systems. This project is aimed at the formalization of several notions in the context of a theoretical framework which serves as the foundation for a comprehensive study on termination analysis. 

Development of Theorem Proving Technologies 

Advances in theorem proving have enabled the emergence of a variety of formal developments that, over the years, have resulted in large corpora of formalizations. For example, the NASA PVS Library is a 30+ years old collection of formal developments written in PVS. The Library contains 55 entries with more than 28000 proofs. Unfortunately, the simple accumulation of entries does not guarantee their reusability. In fact, in logical systems with highly expressive specification languages, it is often the case for a conceptual object to be defined in several different ways. One of the results of this project is the development of a novel technique able to establish proven sound connections between formal definitions. These connections support the possibility of borrowing of proved results between different formalizations, improving their reusability. Several concrete examples taken from the NASA PVS Library were used to illustrate the application of the technique. In particular, we could fix a formalization from the NASA Library that was affected by an upgrade of the prover in a fraction of the time initially estimated for such a task. 

Publications

Mariano M. Moscato, Carlos Gustavo López Pombo, César A. Muñoz, and Marco A. Feliú. “Boosting the Reuse of Formal Specifications”. In: Interactive Theorem Proving – 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings. Ed. by Jeremy Avigad and Assia Mahboubi. Vol. 10895. Lecture Notes in Computer Science. Springer, pp. 477–494. doi: 10.1007/978-3-319-94821-8\_28. url: https://doi.org/10.1007/978-3-319-94821-8%5C_28.

Marco A. Feliú and Mariano M. Moscato. “Towards a Formal Safety Framework for Trajectories”. In: NASA Formal Methods – 10th International Symposium, NFM 2018, Newport News, VA, USA, April 17-19, 2018, Proceedings. Ed. by Aaron Dutle, César A. Muñoz, and Anthony Narkawicz. Vol. 10811. Lecture Notes in Computer Science. Springer, pp. 179–184. doi: 10.1007/978-3-319-77935-5\_13. url: https://doi.org/10.1007/978-3-319-77935-5%5C_13. 

Thiago Mendonça Ferreira Ramos, César A. Muñoz, Mauricio Ayala-Rincón, Mariano M. Moscato, Aaron Dutle, and Anthony Narkawicz. “Formalization of the Undecidability of the Halting Problem for a Functional Language”. In: Logic, Language, Information, and Computation – 25th International Workshop, WoLLIC 2018, Bogota, Colombia, July 24-27, 2018, Proceedings. Ed. by Lawrence S. Moss, Ruy J. G. B. de Queiroz, and Maricarmen Martínez. Vol. 10944. Lecture Notes in Computer Science. Springer, pp. 196–209. doi: 10.1007/978-3-662-57669-4\_11. url: https: //doi.org/10.1007/978-3-662-57669-4%5C_11.

Laura Titolo, Marco A. Feliú, Mariano M. Moscato, and César A. Muñoz. “An Abstract Interpretation Framework for the Round-Off Error Analysis of Floating-Point Programs”. In: Verification, Model Checking, and Abstract Interpretation – 19th International Conference, VMCAI 2018, Los Angeles, CA, USA, January 7-9, 2018, Proceedings. Ed. by Isil Dillig and Jens Palsberg. Vol. 10747. Lecture Notes in Computer Science. Springer, pp. 516–537. doi: 10.1007/978-3-319- 73721-8\_24. url: https://doi.org/10.1007/978-3-319- 73721-8%5C_24.

Laura Titolo, Mariano M. Moscato, César A. Muñoz, Aaron Dutle, and François Bobot. “A Formally Verified Floating-Point Implementation of the Compact Position Reporting Algorithm”. In: Formal Methods – 22nd International Symposium, FM 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 15-17, 2018, Proceedings. Ed. by Klaus Havelund, Jan Peleska, Bill Roscoe, and Erik P. de Vink. Vol. 10951. Lecture Notes in Computer Science. Springer, pp. 364–381. doi: 10.1007/978-3-319-95582- 7\_22. url: https://doi.org/10.1007/978-3-319- 95582-7%5C_22.

Laura Titolo, César A. Muñoz, Marco A. Feliú, and Mariano M. Moscato. “Eliminating Unstable Tests in Floating-Point Programs”. In: CoRR abs/1808.04289. Pre-proceedings of the 28th International Symposium on Logic-based Program Synthesis and Transformation, LOPSTR 2018, Frankfurt am Main, Germany. arXiv: 1808.04289. url: http://arxiv.org/abs/1808.04289.

Aaron Dutle, Mariano M. Moscato, Laura Titolo, and César A. Muñoz. “A Formal Analysis of the Compact Position Reporting Algorithm”. In: Verified Software. Theories, Tools, and Experiments – 9th International Conference, VSTTE 2017, Heidelberg, Germany, July 22-23, 2017, Revised Selected Papers. Ed. by Andrei Paskevich and Thomas Wies. Vol. 10712. Lecture Notes in Computer Science. Springer, pp. 19–34. doi: 10.1007/978-3-319-72308-2\_2. url: https://doi.org/10.1007/978-3-319-72308-2%5C_2.

Mariano M. Moscato, Laura Titolo, Aaron Dutle, and César A. Muñoz. “Automatic Estimation of Verified Floating-Point Round-Off Errors via Static Analysis”. In: Computer Safety, Reliability, and Security – 36th International Conference, SAFECOMP 2017, Trento, Italy, September 13-15, 2017, Proceedings. Ed. by Stefano Tonetta, Erwin Schoitsch, and Friedemann Bitsch. Vol. 10488. Lecture Notes in Computer Science. Springer, pp. 213–229. doi: 10.1007/978-3-319- 66266-4\_14. url: https://doi.org/10.1007/978-3-319-66266-4%5C_14.

Mariano M. Moscato, César A. Muñoz, and Andrew P. Smith. “Affine Arithmetic and Applications to Real-Number Proving”. In: Interactive Theorem Proving – 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings. Ed. by Christian Urban and Xingyuan Zhang. Vol. 9236. Lecture Notes in Computer Science. Springer, pp. 294–309. doi: 10.1007/978-3-319-22102-1\_20. url: https://doi.org/10.1007/978-3-319-22102-1%5C_20.

Mariano M. Moscato, Carlos López Pombo, and Marcelo F. Frias. “Dynamite: A tool for the verification of alloy models based on PVS”. In: ACM Transactions on Software Engineering Methodologies. 23.2, 20:1–20:37. doi: 10.1145/2544136. url: http://doi.acm.org/10.1145/2544136.

Pablo Abad, Nazareno Aguirre, Valeria S. Bengolea, Daniel Ciolek, Marcelo F. Frias, Juan P. Galeotti, Tom Maibaum, Mariano M. Moscato, Nicolás Rosner, and Ignacio Vissani. “Improving Test Generation under Rich Contracts by Tight Bounds and Incremental SAT Solving”. In: Sixth IEEE International Conference on Software Testing, Verification and Validation, ICST 2013, Luxembourg, Luxembourg, March 18-22, 2013. IEEE Computer Society, pp. 21–30. doi: 10.1109/ICST. 2013.46. url: https://doi.org/10.1109/ICST.2013.46.

Manuel Giménez, Mariano M. Moscato, Carlos Gustavo López Pombo, and Marcelo F. Frias. “HeteroGenius: A Framework for Hybrid Analysis of Heterogeneous Software Specifications”. In: Proceedings First Latin American Workshop on Formal Methods, LAFM 2013, Buenos Aires, Argentina, August 26th 2013. Ed. by Nazareno Aguirre and Leila Ribeiro. Vol. 139. EPTCS, pp. 65–70. doi: 10.4204/EPTCS.139.7. url: https: //doi.org/10.4204/EPTCS.139.7.

Mariano M. Moscato, Carlos López Pombo, and Marcelo F. Frias. “Dynamite 2.0: New Features Based on UnSAT-Core Extraction to Improve Verification of Software Requirements”. In: Theoretical Aspects of Computing – ICTAC 2010, 7th International Colloquium, Natal, Rio Grande do Norte, Brazil, September 1-3, 2010. Proceedings. Ed. by Ana Cavalcanti, David Déharbe, Marie-Claude Gaudel, and Jim Woodcock. Vol. 6255. Lecture Notes in Computer Science. Springer, pp. 275–289. doi: 10.1007/978-3-642-14808-8\_19. url: https://doi.org/10.1007/978-3-642-14808-8%5C_19.

Nazareno Aguirre, Marcelo F. Frias, Mariano M. Moscato, T. S. E. Maibaum, and Alan Wassyng. “Describing and Analyzing Behaviours over Tabular Specifications Using (Dyn)Alloy”. In: Fundamental Approaches to Software Engineering, 12th International Conference, FASE 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings. Ed. by Marsha Chechik and Martin Wirsing. Vol. 5503. Lecture Notes in Computer Science. Springer, pp. 155–170. doi: 10.1007/978-3-642-00593-0\_11. url: https://doi.org/10.1007/978-3-642-00593-0%5C_11.

Mariano M. Moscato, Carlos López Pombo, and Marcelo F. Frias. “Lessons Learnt on the Verification of Models Using Dynamite”. International Symposium on Automatic Program Verification APV09; February 15, 2009. Río Cuarto, Córdoba, Argentina.

Marcelo F. Frias, Carlos López Pombo, and Mariano M. Moscato. “Alloy Analyzer+PVS in the Analysis and Verification of Alloy Specifications”. In: Tools and Algorithms for the Construction and Analysis of Systems, 13th International Conference, TACAS 2007, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007 Braga, Portugal, March 24 – April 1, 2007, Proceedings. Ed. by Orna Grumberg and Michael Huth. Vol. 4424. Lecture Notes in Computer Science. Springer, pp. 587–601. doi: 10.1007/978-3-540-71209-1\_46. url: https://doi.org/10.1007/978-3-540-71209-1%5C_46.

Marcelo F. Frias, Carlos López Pombo, and Mariano M. Moscato. “Dynamite: Alloy Analyzer + PVS in the Analysis and Verification of Alloy Specifications”. First Alloy Workshop (co-located with the Fourteenth ACM SIGSOFT Symposium on Foundations of Software Engineering); November 6; Portland, Oregon, USA.