Laura Titolo

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 


Personal Webpage
DBLP 
Google Scholar

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