Dimitra Giannakopoulou, Ph.D.

I am a Research Computer Scientist with the NASA Ames Research Center, and a member of the Robust Software Engineering Group. My work is concerned with applying modular and compositional formal verification techniques to autonomous systems and architectures.

Before joining Ames, I was a Research Associate with the Department of Computing, Imperial College, University of London, UK, working on methods for the specification and automatic verification of distributed systems. I have graduated from the Dept of Computer Engineering and Informatics, University of Patras, Greece. I hold an MSc with distinction from Imperial College, in "Foundations of Advanced Information Technology", and since March 1999, a PhD degree from Imperial College, University of London, thesis title " Model Checking for Concurrent Software Architectures".

[Awards] [Keynotes] [Research/Publications] [Events/Committees] [Projects/Tools]

News

Invited speaker, QEST 2013, 10th International Conference on Quantitative Evaluation of SysTems, Buenos Aires, Argentina.

Program co-chair, CBSE 2013, 16th International ACM Sigsoft Symposium on Component-Based Software Engineering, Vancouver, Canada, June 2013. Abstract submission deadline: Feb 6, 2013.

Giannakopoulou, D., Rakamaric, Z., and Raman, V., “ SAS 2012, Symbolic Learning of Component Interfaces.

Keynotes

"To Scale or Not to Scale: Experience with Formal Methods and NASA Systems". Invited talk at FMICS 2012, 17th International Workshop on Formal Methods for Industrial Critical Systems, Paris France, 2012.

"Automata Generation: *Not* your Usual Machine Learning". Invited talk at MALETS 2011, International Workshop on Machine Learning Technologies in Software Engineering, Lawrence, KS, USA, 2011.

""Fly me to the Moon: Verification of Aerospace Systems"". Invited talk at SEFM 2010, 8th IEEE International Conference on Software Engineering and Formal Methods (SEFM 2010), Pisa, Italy, 2011.

"NASA's State-Space Exploration: Verifying Safety-Critical Systems". Invited talk at SEAA 2009, 35th EUROMICRO conference on Software Engineering and Advanced Applications in Patras, Greece. [Slides] .

Research

I am interested in the design and analysis of distributed and component-based systems, with a focus on model checking and software architectures. Recently, my research has focused on automating assume-guarantee verification by generating assumptions. I have also been working on test-case generation for air-traffic control systems.

Publications

My full list of publications can be found HERE.

Selected Publications

Giannakopoulou, D., Rakamaric, Z., and Raman, V., “ SAS 2012, Symbolic Learning of Component Interfaces.

Giannakopoulou, D, Bushnell, D., Schumann, J., Erzberger, H., Heere, K.: Formal testing for separation assurance. Ann. Math. Artif. Intell. 63(1): 5-30 (2011).

Sébastien C., Giannakopoulou, D., Pecheur,C., Feary, M.: A formal framework for design and analysis of human-machine interaction. SMC 2011.

Giannakopoulou, D., and Pasareanu, C.S., “Interface Generation and Compositional Verification in JavaPathfinder”, FASE 2009.

Giannakopoulou, D., and Pasareanu, C.S., editors. Journal of Formal methods in System Design, special issue on Learning Techniques for Compositional Reasoning, Volume 32, Number 3, Springer, June 2008.

Gheorghiu, M., Pasareanu, C.S., and Giannakopoulou, D. “Automated Assume-Guarantee Reasoning by Abstraction Refinement”, CAV 2008.

Emmi, M., Giannakopoulou, D., and Pasareanu, C.S., “Assume-Guarantee Verification for Interface Automata”, FM’08.

Gheorghiu, M., Giannakopoulou, D., and Pasareanu, C.S. “Refining Interface Alphabets for Compositional Verification”, TACAS 2007.

Giannakopoulou, D., Pasareanu, C., and Cobleigh, J.M. "Assume-guarantee Verification of Source Code with Design-Level Assumptions", ICSE'2004.

Cobleigh, J.M., Giannakopoulou, D., and Pasareanu, C.S. "Learning Assumptions for Compositional Verification", TACAS 2003.

Giannakopoulou, D. and Lerda, F. "From States to Transitions: Improving translation of LTL formulae to Buchi automata", FORTE 2002.

Giannakopoulou, D., Pasareanu, C., and Barringer, H., "Assumption Generation for Software Component Verification", ASE 2002.
Best paper, ACM Sigsoft Distinguished Paper.

Events / Committees

Program co-chair, Conference on Fundamental Approaches to Software Engineering (FASE 2011), European Joint Conferences on Theory and Practice of Software (ETAPS).

Program co-chair, NASA Formal Methods Symposium (NFM 2009).

Co-organizer, Workshop Series on the Specification and Verification of Component-Based Systems (SAVCBS). Affiliated with ACM SIGSOFT Symposium on Foundations of Software Engineering (FSE) since 2003.

The full list of committees that I have served can be found HERE.

Upcoming Committees:

2nd NASA Formal Methods Symposium (NFM 2010).

32nd International Conference on Software Engineering (ICSE 2010). PC member for main technical/research track and research demo track.

Conference on Fundamental Approaches to Software Engineering (FASE 2010), European Joint Conferences on Theory and Practice of Software (ETAPS).

Past Committees:

Track on New Ideas and Emerging Results, 31st International Conference on Software Engineering (ICSE 2009).

7th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE 2009).

Conference on Fundamental Approaches to Software Engineering (FASE 2009), European Joint Conferences on Theory and Practice of Software (ETAPS).

23rd IEEE/ACM International Conference on Automated Software Engineering (ASE 2008).

16th ACM SIGSOFT International Symposium on Foundations of Software Engineering (ACM SIGSOFT 2008 / FSE 16).

15th International Symposium on Formal Methods (FM’08).

Conference on Fundamental Approaches to Software Engineering (FASE 2008), European Joint Conferences on Theory and Practice of Software (ETAPS).