Laura Titolo
Senior Research Scientist
NASA-NIA Formal Methods Team,
Safety Critical
Avionics System Branch
Tel: (757) 325-6905
Email: laura.titolo@nianet.org or laura.titolo@nasa.gov
Biography
Dr. Titolo is a Research Scientist at the National Institute of Aerospace working in the Safety-Critical Avionics Systems Branch at NASA Langley Research Center. She received her Ph.D. in Computer Science from the University of Udine (Italy) in May 2014. Her Ph.D. thesis was in part carried out at the Technical University of Valencia (Spain). She earned a Bachelor’s and a Master’s degree in Computer Science from the University of Udine, both received with full marks and honors (summa cum laude). She was a student at the scientific class of the Scuola Superiore dell’Università of Udine (an excellence University program for talented students), and received her degree in June 2011 with full marks and honors.
Dr. Titolo’s research interests include every aspect of formal methods. In particular, she works on developing new tools for the formal verification and analysis of safety-critical avionics applications. She is currently working on improving the reliability of airspace software involving finite-precision computations.
Education
- Ph.D. in Computer Science, University of Udine (Italy), 2014
- Master Degree in Computer Science, University of Udine (Italy), Summa cum laude, 2010
- Bachelor Degree in Computer Science, University of Udine (Italy), Summa cum laude, 2008
- Scientific Curriculum Diploma, Scuola Superiore (University Insitute for talented students) of the University of Udine (Italy), Summa cum laude, 2010
Work Experience
- Research Scientist II, National Institute of Aerospace, 2017-present
- Postdoctoral Research Scholar, National Institute of Aerospace, 2015-2017
- Postdoctoral Researcher, University of Malaga (Spain), 2014-2015
- Research Scholar, University of Valencia, 2009-2010
Research Areas/Expertise
- Formal Methods, Static Analysis and Verification
- Abstract Interpretation
- Numerical Analysis of Finite Precision Computations
- Analysis of Concurrent and Reactive Systems
- Computational Logic
- Formal Semantics of Programming Languages
Publications
Mariano M. Moscato, Laura Titolo, Marco A. Feliú, César A. Muñoz: Probably Correct Floating-Point Implementation of a Point-in-Polygon Algorithm, 3rd World Congress on Formal Methods (FM 2019), Lecture Notes in Computer Science, Vol. 11800, 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, 11th International Symposium on NASA Formal Methods (NFM 2019), Lecture Notes in Computer Science, Vol. 11460, 2019
Laura Titolo, César A. Muñoz, Marco A. Feliú, Mariano M. Moscato, Eliminating Unstable Tests in Floating-Point Programs, 28th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2018), Lecture Notes in Computer Science, Vol. 11408, 2019
Laura Titolo, Mariano Moscato, Cesar A. Muñoz, Aaron Dutle, Francois Bobot, A Formally Verified Floating-Point Implementation of the Compact Position Reporting Algorithm, 22nd International Symposium on Formal Methods (FM 2018), Lecture Notes in Computer Science, Vol. 10951, pp. 364-381, 2018
Laura Titolo, Marco A. Feliu, Mariano Moscato, Cesar A. Muñoz, An Abstract Interpretation Framework for the Round-Off Error Analysis of Floating-Point Programs, 19th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2018), Lecture Notes in Computer Science, Vol. 10747, pp. 516-537, 2018
Mariano Moscato, Laura Titolo, Aaron Dutle, Cesar A. Muñoz, Automatic Estimation of Verified Floating-Point Round-Off Errors via Static Analysis, 36th International Conference on Computer Safety, Reliability, and Security (SAFECOMP 2017), Lecture Notes in Computer Science, Vol. 10488, pp. 213-229, 2017
Aaron Dutle, Mariano Moscato, Laura Titolo, Cesar A. Muñoz, A Formal Analysis of the Compact Position Reporting Algorithm, Proceedings of the 9th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2017), Lecture Notes in Computer Science, Vol. 10712, pp. 19-34, 2017
Maria del Mar Gallardo, Leticia Lavado, Laura Panizo, Laura Titolo. A Constraint-based Language to Model Intelligent Environments, in Journal of Reliable Intelligent Environments, Volume 3, Issue 1, pp 55-79, Springer, 2017
Marco Comini, Maria del Mar Gallardo, Laura Titolo, Alicia Villanueva, A program analysis framework for tccp based on abstract interpretation, in Formal Aspects of Computing, Volume 29, Issue 3, pp 531–557, Springer, 2017
Marco Comini, Maria del Mar Gallardo, Laura Titolo, Alicia Villanueva, Abstract analysis of universal properties for tccp, 25th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2015), Selected Revised Papers, Lecture Notes in Theoretical Computer Science, Vol. 9527, pp. 163–178, 2015
Maria del Mar Gallardo, Laura Panizo, Laura Titolo, A discretized operational semantics for the implementation of hy-tccp, Proceedings of the XV Conference on Programming and Languages (PROLE 2015), 2015
Damian Adalid, Maria del Mar Gallardo, Laura Titolo, Modeling Hybrid Systems in the Concurrent Constraint Paradigm, Selected paper from the XV Conference on Programming and Languages (PROLE 2014), Electronic Proceedings in Theoretical Computer Science (EPTCS), Vol. 173, pages 1-15, 2014
Damian Adalid, Maria del Mar Gallardo, Laura Titolo, Modeling Hybrid Systems in Hy-tccp, Proceedings of the 3rd International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2014), 2014
Marco Comini, Laura Titolo, Alicia Villanueva, Abstract Diagnosis for tccp using a Linear Temporal Logic, in Theory and Practice of Logic Programming (TPLP) Volume 14, Issue 4-5, Special Issue of the 30th International Conference on Logic Programming, pp 787-801, Cambridge University Press, 2014
Laura Titolo, An Abstract Interpretation Framework for Verification of Timed Concurrent Constraint Languages, in on-line supplement of the journal Theory and Practice of Logic Programming (TPLP), Volume 13, Issue 4-5, Cambridge University Press, 2013
Marco Comini, Laura Titolo, Alicia Villanueva, Towards an Effective Decision Procedure for LTL formulas with Constraints, Proceedings of the 23rd Workshop on Logic-based methods in Programming Environments (WLPE 2013), 2013
Marco Comini, Laura Titolo, Alicia Villanueva, Abstract Diagnosis for Timed Concurrent Constraint programs, Theory and Practice of Logic Programming (TPLP) Volume 11, Issue 4-5, Special Issue of the 28th International Conference on Logic Programming, pp 487-502, Cambridge University Press, 2011