NASA Logo, National Aeronautics and Space Administration

Publications

Books

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.

Tutorials

Giannakopoulou, D., and Pasareanu, C.S. “Automated Techniques for Compositional Verification”. Proceedings of the 30th International Conference on Software Engineering (ICSE’2008), Leipzig, Germany, May 2008.

Journals

  • Giannakopoulou, D, Bushnell, D., Schumann, J., Erzberger, H., Heere, K.: Formal testing for separation assurance. Ann. Math. Artif. Intell. 63(1): 5-30 (2011).
  • Giannakopoulou, D., Pasareanu, C.S. and Blundell, C. “Assume-Guarantee Testing for Software Components”. IET Software Journal.
  • Pasareanu, C.S., Giannakopoulou, D., Gheorghiu, M., Cobleigh, J.M., and Barringer, H. “Learning to Divide and Conquer: Applying the L* Algorithm to Automate Assume-Guarantee Reasoning”.Journal of Formal methods in System Design, special issue on Compositional Reasoning, Springer.
  • Giannakopoulou, D., Pasareanu, C.S., and Barringer, H., "Component Verification with Automatically Generated Assumptions". Journal of Automated Software Engineering, Kluwer Academic Publishers, Volume 12, Issue 3, July 2005.
  • Guillaume Brat, Dimitra Giannakopoulou, Allen Goldberg, Klaus Havelund, Mike Lowry, Corina Pasareanu, Arnaud Venet, Willem Visser, Rich Washington. "Experimental Evaluation of VV Tools on Martian Rover Software". Journal of Formal Methods in System Design, Kluwer Academic Publishers, Volume 25, Issue 2-3, September-November 2004.
  • Giannakopoulou, D., Kramer, J., and Cheung, S.C. "Behaviour Analysis of Distributed Systems Using the Tracta Approach". Journal of Automated Software Engineering, special issue on Automated Analysis of Software, vol.6(1), January 1999. R. Cleaveland and D. Jackson, Eds, Kluwer Academic Publishers.

Conferences and Workshops

[2014]

  • Christian von Essen, Dimitra Giannakopoulou: Analyzing the Next Generation Airborne Collision Avoidance System. TACAS 2014.
  • Dimitra Giannakopoulou, Falk Howar, Malte Isberner, Todd Lauderdale, Zvonimir Rakamaric, Vishwanath Raman: Taming Test Inputs for Separation Assurance. ASE 2014.
  • [2013]

  • Falk Howar, Dimitra Giannakopoulou, Zvonimir Rakamaric: Hybrid learning: interface generation through static, dynamic, and symbolic analysis. ISSTA 2013.
  • Dimitra Giannakopoulou, Corina S. Pasareanu: Abstraction and Learning for Infinite-State Compositional Verification. Festschrift for Dave Schmidt 2013.
  • [2012]

  • Giannakopoulou, D., Rakamaric, Z., and Raman, V. : Symbolic Learning of Component Interfaces. SAS 2012.
  • [2011]

  • Domenico Bianculli, Dimitra Giannakopoulou, Corina S. Pasareanu: Interface decomposition for service compositions. ICSE 2011.
  • Sébastien C., Giannakopoulou, D., Pecheur,C., Feary, M.: A formal framework for design and analysis of human-machine interaction. SMC 2011.
  • Dimitra Giannakopoulou, Neha Rungta, Michael Feary: Automated test case generation for an autopilot requirement prototype. SMC 2011.
  • Dimitra Giannakopoulou, Corina S. Pasareanu: Context Synthesis. SFM 2011.
  • [2010]

  • Rishabh Singh, Dimitra Giannakopoulou, Corina S. Pasareanu: Learning Component Interfaces with May and Must Abstractions. CAV 2010.
  • Dimitra Giannakopoulou: "Fly Me to the Moon": Verification of Aerospace Systems. SEFM 2010.
  • [2009]

    Giannakopoulou, D., and Pasareanu, C.S., “Interface Generation and Compositional Verification in JavaPathfinder”. Proceedings of the ETAPS conference on Fundamental Approaches to Software Engineering (FASE 2009), York, UK, March 2009.

    [2008]

    Gheorghiu, M., Pasareanu, C.S., and Giannakopoulou, D. “Automated Assume-Guarantee Reasoning by Abstraction Refinement”. Proceedings of the 20th International Conference on Computer Aided Verification (CAV 2008), Princeton, USA, July 2008.

    Emmi, M., Giannakopoulou, D., and Pasareanu, C.S., “Assume-Guarantee Verification for Interface Automata”. Proceedings of the 15th International Symposium on Formal Methods (FM’08), Turku, Finland, May 2008.

    [2007]

    Gheorghiu, M., Giannakopoulou, D., and Pasareanu, C.S. “Refining Interface Alphabets for Compositional Verification”. Proceedings of the 13th International Conference for the Construction and Analysis of Systems (TACAS 2007), Braga, Portugal, March 2007.

    [2006]

    Pasareanu, C.S., and Giannakopoulou, D. "Towards a Compositional SPIN". Proceedings of the 13th International SPIN Workshop on Model Checking of Software (SPIN'06), Vienna, Austria, March-April 2006.

    Brat, G. Gheorghiu, M. Giannakopoulou, D. and Pasareanu, C. “Verification of Plans and Procedures”. IEEE Aerospace Conference, Big Sky, Montana, March 2006.

    Brat, G., Denney, E., Giannakopoulou D., and Jonsson, A. "Verification of Autonomous Systems for Space Applications". IEEE Aerospace Conference, Big Sky, Montana, March 2006.

    Brat, G., Denney, E., Farell, K., Giannakopoulou D., Jonsson, A., Frank, J., Boddy, M., Carpenter, T., and Estlin, T. "A Robust Compositional Architecture for Autonomous Systems". IEEE Aerospace Conference, Big Sky, Montana, March 2006.

    [2005]

    Blundell, C., Giannakopoulou, D., and Pasareanu, C.S. "Assume-Guarantee Testing". 4th Workshop on Specification and Verification of Component-Based Systems (SAVCBS�05), associated with the 5th joint meeting of the European Software Engineering Conference and ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE 2005), September 2005.

    Giannakopoulou, D. and Pasareanu, C.S. "Learning-Based Assume-Guarantee Verification" (Tool Paper), in Proc. of the 12th International SPIN Workshop on Model Checking of Software (SPIN 2005), San Francisco, USA, August 2005.

    Giannakopoulou, D., Pasareanu, C.S., Lowry, M., Washington, R. "Lifecycle Verification of the NASA Ames K9 Rover Executive", ICAPS'05 Workshop on Verification and Validation of Model-Based Planning and Scheduling Systems (VVPS'05), Monterey, California, June 2005.

    [2004]

    Giannakopoulou, D., Pasareanu, C., and Cobleigh, J.M. "Assume-guarantee Verification of Source Code with Design-Level Assumptions", Proc. of the 26th International Conference on Software Engineering (ICSE'2004), Edinburgh, Scotland, May 2004 (acceptance rate 13%).

    [2003]

    Giannakopoulou, D. and Magee, J. "Fluent Model Checking for Event-Based Systems", in Proc. of the 4th joint meeting of the European Software Engineering Conference and ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE 2003), September 2003, Helsinki, Finland (acceptance rate 19%).

    Barringer, H., Giannakopoulou, D., and Pasareanu, C.S. "Proof Rules for Automated Compositional Verification through Learning". 2nd Workshop on Specification and Verification of Component-Based Systems (SAVCBS'03), associated with the 4th joint meeting of the European Software Engineering Conference and ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE 2003).

    Cobleigh, J.M., Giannakopoulou, D., and Pasareanu, C.S. "Learning Assumptions for Compositional Verification", in Proc. of the 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2003). April 2003, Warsaw, Poland. Springer, LNCS (acceptance rate 25%).

    Guillaume Brat, Dimitra Giannakopoulou, Allen Goldberg, Klaus Havelund, Mike Lowry, Corina Pasareanu, Arnaud Venet, Willem Visser. "Experimental Evaluation of VV Tools on Martian Rover Software". SEI Software Model Checking Workshop, March 2003, invited.

    [2002]

    Giannakopoulou, D. and Lerda, F. "From States to Transitions: Improving translation of LTL formulae to B automata", in Proc. of the 22nd IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems (FORTE 2002). November 2002, Houston, Texas. Springer, Lecture Notes in Computer Science.

    Giannakopoulou, D., Pasareanu, C., and Barringer, H., "Assumption Generation for Software Component Verification", in Proc. ofthe 17th IEEE International Conference on Automated Software Engineering (ASE 2002). September 2002, Edinburgh, UK acceptance rate 20%).
    Awards. Best paper, ACM Sigsoft Distinguished Paper.

    [2001]

    Giannakopoulou, D. and Havelund, K. "Automata-Based Verification of Temporal Properties on Running Programs", in Proc. of the 16th IEEE International Conference on Automated Software Engineering (ASE 2001). November 2001, San Diego, USA. Full version available as a technical report.

    Giannakopoulou, D. and Penix, J., "Component Verification and Certification in NASA Missions", in Proc. of the 4th ICSE Workshop on Component-Based Software Engineering: Component Certification and System Prediction, Toronto, Canada, May 2001.

    [2000]

    Karamanolis, C., Giannakopoulou D., Magee, J., and Wheater, S., "Model Checking of Workflow Schemas". In Proc. of the 4th International Conference on Enterprise Distributed Object Computing (EDOC 2000), Makuhari, Japan, IEEE Computer Society, September 2000.

    Magee, J., Pryce, N., Giannakopoulou, D., and Kramer, J., "Graphical Animation of Behavior Models", in Proc. of the 22d International Conference on Software Engineering (ICSE'2000), Limerick, Ireland, June 2000 (acceptance rate < 15%).

    [1999]

    Giannakopoulou, D., Magee, J., and Kramer, J. "Checking Progress with Action Priority: Is it Fair?" in Proc. of the 7th European Software Engineering Conference held jointly with the 7th ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE'99), Toulouse, France, September 1999. Lecture Notes in Computer Science 1687, pp.511-527. O. Nierstrasz and M. Lemoine, Eds.

    Magee, J., Kramer, J., and Giannakopoulou, D. "Behaviour Analysis of Software Architectures," in Proc. of the 1st Working IFIP Conference on Software Architecture (WICSA1), San Antonio, TX, USA, 22-24 February 1999.

    [1998]

    Magee, J., Kramer, J., and Giannakopoulou, D. "Software Architecture Directed Behaviour Analysis," in Proc. of the Ninth IEEE International Workshop on Software Specification and Design (IWSSD-9), Ise-shima, Japan, April 16-18 1998, pp. 144-146.

    Giannakopoulou, D., Kramer, J., and Magee, J. "Behaviour Analysis Based on Software Architecture," in Proc. of the International Workshop on the Role of Software Architecture in Testing and Analysis (ROSATEA), Marsala, Sicily, Italy, June 1998. D. Richardson, P. Inverardi, and A. Bertolino, Eds, invited.

    Giannakopoulou, D., Kramer, J., and Magee, J. "Practical Behaviour Analysis for Distributed Software Architectures". UK Programmable Networks and Telecommunications Workshop, Hewlett-Packard Laboratories, Bristol. September 1998, invited.

    [1997]

    Magee, J., Kramer, J., and Giannakopoulou, D. "Analysing the Behaviour of Distributed Software Architectures: a Case Study," in Proc. of the 5th IEEE Workshop on Future Trends of Distributed Computing Systems, Tunis, Tunisia, October 1997, pp. 240-245.

    Cheung, S.C., Giannakopoulou, D., and Kramer, J. "Verification of Liveness Properties using Compositional Reachability Analysis," in Proc. of the 6th European Software Engineering Conference held jointly with the 5th ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE'97), Zurich, Switzerland, September 1997. Lecture Notes in Computer Science 1301, pp.227-243. M. Jazayeri and H. Schauer, Eds.

    Giannakopoulou, D., and Kramer, J. "An Integrated Environment for the Design and Analysis of Distributed Systems", 3d Cabernet Plenary Workshop, Rennes, France, 16-18 April 1997.

    Giannakopoulou, D., Kramer, J., and Cheung, S.C. "Tracta: An Environment for Analysing the Behaviour of Distributed Systems," in Proc. of the 1st ACM Sigplan Workshop on Automated Analysis of Software (AAS'97), Paris, France, January 1997, pp. 113-125. R. Cleaveland and D. Jackson, Eds.

    Awards. Selected as one of three best papers of workshop, extended versions of which have been published in the ASE journal.

    Research Reports

    Giannakopoulou, D. and Lerda, F., “Efficient translation of LTL formulae into B automata”, RIACS/USRA Technical Report, 01.29, June 2001.

    Giannakopoulou, D. and Havelund, K., “Runtime Analysis of Linear Temporal Logic Specifications”, RIACS/USRA, Technical Report, 01.21, August 2001.

    Karamanolis, C., Giannakopoulou, D., Magee, J., and Wheater, S. “Modelling and Analysis of Workflow Processes”, Dept. of Computing, Imperial College, London, Research Report, May 2000.

    Giannakopoulou, D. “Modelling and Analysis of the Bounded Retransmission Protocol: Experience with Discrete Time”, Imperial College, London, Research Report, 2000.

    Giannakopoulou, D.“The Tracta Approach for Behaviour Analysis of Concurrent Systems,” Dept. of Computing, Imperial College, London, Research Report, September 1995.

    Giannakopoulou, D., and Hadzilacos, T. “Modelling Geographic Applications with Objects: Promises and Limitations,” Computer Technology Institute Technical Report, March 1994.

    Theses


    Giannakopoulou, D. “Model Checking for Concurrent Software Architectures”, PhD Thesis, Imperial College of Science Technology and Medicine, University of London, March 1999.

    Giannakopoulou, D. “Voting Algorithms for Replicated Data”, MSc Thesis, Imperial College of Science Technology and Medicine, University of London, Sept 1994.

    Giannakopoulou, D. “The Object-Oriented Approach for Geographic Databases”, Diploma Thesis, Department of Computer Engineering and Informatics, University of Patras, Greece, February 1993.

    First Gov logo
    NASA Logo - nasa.gov