NASA Logo, National Aeronautics and Space Administration

Corina Pasareanu, Ph.D.

I am doing research in software engineering at NASA Ames, in the Robust Software Engineering group. I am employed by Carnegie Mellon University, at the Silicon Valley campus. I am affiliated with CMU CyLab and also hold a courtesy appointment with CMU ECE. Research interests:
  • Model checking and automated testing: I investigate the use of abstraction and symbolic execution in the context of Java PathFinder, with applications to test input generation and error detection. Together with many collaborators, I have developed Symbolic PathFinder (SPF, jpf-symbc), a symbolic execution tool for Java bytecode. See NASA article on the use of SPF in industry.
  • Compositional verification: I also work on using learning and abstraction techniques for automating assume-guarantee style compositional verification. Recently I have worked on compositional techniques for probabilistic systems and I am currently investigating hybrid systems.
  • Model-based development: Together with collaborators from Vanderbilt University and University of Minnesota, we have developed modeling and analysis techniques for multiple statechart formalisms used in the development of NASA systems. See the Polyglot tool-set.
  • Probabilistic software analysis: Recently I have started to investigate probabilistic techniques for the analysis of software components placed in stochastic environments. See project webpage.
  • Autonomy: I was part of the core team that developed PLEXIL, a plan execution language and system for automation. I am now interested in planning for safe surface operations for autonomous vehicles.


Program co-chair for CAV 2015. We welcome your papers!

ICSE 2010 Most Influential Paper Award and ACM SIGSOFT Impact Paper Award for “Bandera: Extracting Finite-state Models from Java Source Code", by James C. Corbett, Matthew B. Dwyer, John Hatcliff, Shawn Laubach, Corina S. Pasareanu, Robby, and Hongjun Zheng, ICSE 2000.

Recently, I was general chair for ISSTA 2014 and program co-chair for PASTE 2013.

Invited talk at VSSE'13 (ETAPS'13) on "Memoized Symbolic Execution". Lectures at International Summer School Marktoberdorf, Germany, 2012. Lectures at SRI Formal Methods school, 2012. Keynote Speaker at Test & Proof TAP'12.

Program Committee for: POPL'16, TACAS'16, ICSE'16, ISEC'16, FSE'16, ISSTA'15, ASE'15, NFM'15, TACAS'15, SEFM'15, ASE'14, CAV'14, TACAS'14, SEFM'14, FACS'14, ICTAC'14, HVC'14, FMICS'13, TACAS'13, CAV'13, ESEC/FSE'13, ASE'13, NFM'13, FACS'13, BYTECODE'13, CSTVA'13, ICSE-MP'13, FACS'12 (program co-chair), ISSTA'12, SPIN'12, NFM'12, FSE'12 (New Ideas), ISOLA'12, CSTVA'12, VMCAI'12, VSTTE'12, ESEC/FSE'11, ISSTA'11, FASE'11, SPIN'11, VVPS'11, NFM'11, VMCAI'11, FACS'11, ASE'11 (program co-chair). Associate editor for the IEEE TSE journal. Steering Committee for ISSTA, ASE, NFM and FACS.

Some recent presentations related to symbolic execution and Symbolic Pathfinder: ICSE'11 Tech Briefing, ICSE'11 Impact Project, ISSTA'11 Mixed Concrete-Symbolic Solving.

Tutorials: Symbolic PathFinder (ISSTA'10), Compositional Verification (ICSE'08, ASE'10, UC Berkeley).

Selected Publications

  • Compositional Solution Space Quantification for Probabilistic Software Analysis. Mateus Borges, Antonio Filieri, Marcelo D'Amorim, Corina S. Pasareanu, Willem Visser. In PLDI 2014.
  • Statistical Symbolic Execution with Informed Sampling, Antonio Filieri, Corina S. Păsăreanu, Willem Visser, and Jaco Geldenhuys. In FSE 2014.
  • Exact and Approximate Probabilistic Symbolic Execution for Nondeterministic Programs, Kasper Luckow, Corina S. Pasareanu, Matt Dwyer, Antonio Filieri, Willem Visser. In ASE 2014.
  • Quantifying Information Leaks using Reliability Analysis, Quoc-Sang Phan, Pasquale Malacaria, Corina Pasareanu and Marcelo D'Amorim. In SPIN 2014 (short).
  • Assume-Guarantee Abstraction Refinement Meets Hybrid Systems, Sergiy Bogomolov, Goran Frehse, Marius Greitschus, Radu Grosu, Corina Pasareanu, Andreas Podelski and Thomas Strump. In HVC 2014 (best paper award).
Symbolic Execution and Testing: Compositional Verification: Abstraction: PhD Thesis: Abstraction and Modular Reasoning for the Verification of Software.
Here is a list of my publications. See also DBLP.

Class on Software Verification and Testing at CMU SV. International Summer School Marktoberdorf, Germany.
Old Bucharest.


Corina Pasareanu, Ph.D.

NASA Ames Research Center
Mail Stop 269-2
Moffett Field, CA 94035

Phone: +1 (650) 604-4767
Fax:     +1 (650) 604-3594

Email: Corina.S.Pasareanu "at"

First Gov logo
NASA Logo -