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. Research interests:
  • Model checking and automated testing: I investigate the use of abstraction and symbolic execution in the context of the Java PathFinder verification tool set, with applications to test input generation and error detection. Together with many collaborators, I have developed Symbolic PathFinder (jpf-symbc), a symbolic execution tool for Java bytecode.
  • 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 for safety-critical systems: Together with collaborators from Vanderbilt University and University of Minnesota, we have developed modeling and analysis techniques for multiple statechart formalisms used in the model-based development of new NASA systems. See the Polyglot tool-set.
  • Probabilistic software analysis: Recently I have started to investigate probabilistic analysis techniques for computing the reliability of software components placed in stochastic environments. See project webpage.


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.

Program Co-Chair for PASTE 2013.

General chair for ISSTA 2014. Program co-chair for CAV 2015.

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: 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 ACM TOSEM journal. Steering Committee for 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


  • Symbolic PathFinder: Integrating Symbolic Execution with Model Checking for Java Bytecode Analysis, Corina S. Pasareanu, Willem Visser, David Bushnell, Jaco Geldenhuys, Peter Mehlitz, Neha Rungta. In Automated Software Engineering Journal, Springer, 2013
  • Memoise: A Tool for Memoized Symbolic Execution, Guowei Yang, Sarfraz Khurshid, Corina S. Pasareanu. In ICSE 2013 Formal Demo.
  • Compositional Symbolic Execution through Program Specialization, José Miguel Rojas and Corina S. Păsăreanu. In BYTECODE'13 (ETAPS'13).
  • Reliability Analysis in Symbolic Pathfinder, Antonio Filieri, Corina S. Păsăreanu, and Willem Visser. In ICSE 2013.
  • Polyglot: Systematic Analysis for Multiple Statechart Formalisms (tool demo), Corina Pasareanu, Daniel Balasubramanian, Gabor Karsai and Michael Lowry. In TACAS 2013.
  • Symbolic Quantitative Information Flow, Quoc-Sang Phan, Pasquale Malacaria, Oksana Tkachuk and Corina S. Pasareanu. In JPF Workshop 2012.
  • Abstract Pathfinder, Artem Khyzha, Pavel Parizek and Corina Pasareanu. In JPF Workshop 2012.
  • Testing Android Apps Through Symbolic Execution, Nariman Mirzaei, Sam Malek, Corina Pasareanu, Naeem Esfahani and Riyadh Mahmood. In JPF Workshop 2012.
  • Improving Symbolic Execution for Statechart Formalisms, D. Balasubramanian, C. Pasareanu, M. Whalen, G. Karsai, M. Lowry. In MoDeVVa 2012.
  • Memoized Symbolic Execution, Guowei Yang, Corina S. Pasareanu and Sarfraz Khurshid, in ISSTA 2012.
  • Learning Probabilistic Systems from Tree Samples, Anvesh Komuravelli, Corina S. Pasareanu and Edmund M. Clarke, in LICS 2012.
  • Assume-Guarantee Abstraction Refinement for Probabilistic Systems, Anvesh Komuravelli, Corina S. Pasareanu and Edmund M. Clarke, in CAV 2012.
  • Symbolic Execution with Interval Constraint Solving and Meta-Heuristic Search, Mateus Borges, Marcelo D'Amorim, Saswat Anand, David Bushnell and Corina Pasareanu, in ICST 2012.
  • Integrating Statechart Components in Polyglot, Daniel Balasubramanian, Corina Pasareanu, Gabor Karsai, Thomas Pressburger, Michael Lowry and Jason Biatek, in NFM 2012
  • Symbolic Execution Enhanced System Testing, Misty Davies, Corina S. Pasareanu, Vishwanath Raman, in VSTTE 2012.

Symbolic Execution and Testing:

Compositional Verification:


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 -