Laura Titolo


National Institute of Aerospace

NASA LaRC Formal Methods Team

 
 

I am a research scientist at the National Institute of Aerospace and member of the NASA LaRC Formal Method Team at the Langley Research Center (Hampton, Virginia).


From September 2014 to August 2015 I was a postdoctoral researcher in the Mobile Networks and Software Reliability Lab. at the University of Malaga.


I received my Ph.D. in Computer Science from the University of Udine (Cycle XXVII) in May 2014, under the supervision of Marco Comini and Alicia Villanueva.

I received my Bachelor's degree (Laurea Triennale) and Master’s degree (Laurea Specialistica) in Computer Science at the University of Udine, in July 2008 and October 2010, respectively, both with full marks and honors (110/110 cum laude).

I was also a student of the scientific class of the Scuola Superiore dell’Università degli studi di Udine, a complementary University program for talented students, and I received the diploma in June 2011 with full marks and honors (110/110 cum laude).


Here you can find my full cv, and here my list of publications in DBLP.

 

Short biography

Research interests

Publications

I’m interested in:


- analysis of finite precision computations

  1. -semantics of declarative languages

  2. -abstract interpretation

  3. -automatic verification and analysis of concurrent, real-time and hybrid systems

  4. -logic and constraint programming

L. Titolo, M.M. Moscato, C.A. Muñoz, A. Dutle and F. Bobot:

A Formally Verified Floating-Point Implementation of the Compact Position Reporting Algorithm.
22nd International Symposium on Formal Methods (FM 2018), Oxford, UK, 2018.


L. Titolo, M.A. Feliú, M.M. Moscato,  C.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), 516-537, Los Angeles, USA, 2018.


M.M. Moscato, Laura Titolo, A. Dutle, C.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), 213-229, Trento, Italy, 2017.


A. Dutle, M.M. Moscato, L. Titolo, C.A. Muñoz:

A Formal Analysis of the Compact Position Reporting Algorithm.
9th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2017), 19-34, Heidelberg, Germany, 2017.


M.M. Gallardo, L. Lavado, L. Panizo, L. Titolo:
A Constraint- based Language to Model Intelligent Environments.
Journal on Reliable Intelligent Environments (2017) 3: 55, Springer.


M. Comini, M.M. Gallardo, L. Titolo, A. Villanueva:

A program analysis framework for tccp based on abstract interpretation.
Journal on Formal Aspects of Computing 28(3): 531-557 (2017).


  1. M.Comini, M.M. Gallardo, L. Titolo, A. Villanueva:

Abstract Analysis of Universal Properties for tccp.
25th International Symposium of Logic-Based Program Synthesis and Transformation (LOPSTR 2015), Siena, Italy, 2015.


M.M. Gallardo, L. Panizo, L. Titolo:
A discrete operational semantics for the implementation of hytccp.
XV Jornadas sobre Programación y Lenguajes (PROLE 2015), Santander, Spain, 2015.


D. Adalid, M.M. Gallardo, L.Titolo:
Modeling Hybrid Systems in Hy-tccp.
3rd International Conference on Formal Methods on Safety-Critical Systems (FTSCS 2014) Luxembourg, 2014.

                     Available: PDF


D. Adalid, M.M. Gallardo, L.Titolo:
Modeling Hybrid Systems in the concurrent constraint paradigm.

Electronic Proceedings in Theoretical Computer Science volume 173, pp. 1-15.

                    Available: PDF


M. Comini, L.Titolo, A. Villanueva:
Abstract Diagnosis for tccp using a linear temporal logic.
Theory and Practice of Logic Programming, volume 11, issue 4-5, pp. 487-502, Special issue on 27th International Conference on Logic Programming (ICLP 2014).
                     Available: PDF


L.Titolo:
An abstract interpretation framework for verification of Timed Concurrent Constraint Programming.
9th ICLP Doctoral Consortium, Istanbul, Turkey, 2013.
                     Available: PDF


M. Comini, L.Titolo, A. Villanueva:
Toward an effective decision procedure for LTL formulas with constraints.
23rd Workshop on Logic-Based Methods in Programming Environments (WLPE 2013), Istanbul, Turkey, 2013 .
                     Available: PDF


M. Comini, L.Titolo, A. Villanueva:
Abstract Diagnosis for Timed Concurrent Constraint programs.
Theory and Practice of Logic Programming, volume 11, issue 4-5, pp. 487-502, Special issue on 27th International Conference on Logic Programming (ICLP 2011).
                    Available: PDF


PhD Thesis:
An abstract interpretation framework for Diagnosis and Verification of Timed Concurrent Constraint Languages (12th May 2014).

                     Available: PDF



Disclaimer: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All people copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. In most cases, these works may not be reposted without the explicit permission of the copyright holder.