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. My research area is software verification. 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. Currently, my main interest is in developing, extending and maintaining Symbolic PathFinder (jpf-symbc), a symbolic execution tool for Java bytecode. I am also working on using learning techniques for automating assume-guarantee compositional verification. Currently I am working on compositional techniques for probabilistic systems. My research interests also include parallelization of verification tasks and modeling and analysis for multiple statechart formalisms.

Events

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.

Lectures at International Summer School Marktoberdorf, Germany, 2012. Lectures at SRI Formal Methods school, 2012. Keynote Speaker at Test & Proof TAP'12.

Program Co-Chair for FACS'12. Please submit your papers!

Program Committee for: TACAS'13, 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).

Tools

• Symbolic PathFinder (jpf-symbc) (symbolic execution for Java bytecode)
• ASSERT (concolic execution for C code)
• Polyglot (analysis and test case generation for multiple statechart formalisms)
• Abstract PathFinder (data abstraction for Java bytecode analysis)

Selected Publications

Recent:

• 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:

• Differential Symbolic Execution, S. Person, M. Dwyer, S. Elbaum, C. S. Pasareanu, in FSE'08.
• Combining Unit-level Symbolic Execution and System-level Concrete Execution for Testing NASA Software, C. S. Pasareanu, P. C. Mehlitz, D. H. Bushnell, K. Gundy-Burlet, M. Lowry, S. Person, M. Pape, in ISSTA'08.
• Symbolic Execution and Model Checking for Testing, Corina S. Pasareanu, Willem Visser, in Haifa Verification Conference 2007, LNCS 4899: 17-18 (IBM HVC Award).

Compositional Verification:

• Interface Generation and Compositional Verification in JavaPathfinder, D. Giannakopoulou, C. S. Pasareanu, in FASE'09. Correction: Computed interfaces are not most permissive as claimed (thanks: Chang-Seo Park).
• Automated Assume-Guarantee Reasoning by Abstraction Refinement, M. Gheorghiu Bobaru, C. S. Pasareanu, D. Giannakopoulou, in CAV'08.
• Learning to Divide-and-Conquer: Applying the L* Algorithm to Automate Assume-Guarantee Reasoning, Corina S. Pasareanu, Dimitra Giannakopoulou, Mihaela Gheorghiu Bobaru, Jamieson M. Cobleigh, Howard Barringer, in FMSD Journal, 37 pages, Volume 32 , Issue 3 (June 2008), Pages: 175 - 205, Kluwer Academic Publishers.

Abstraction:

• Symbolic Execution with Abstraction, Saswat Anand, Corina S. Pasareanu, Willem Visser, in STTT, Volume 11, Number 1 / February, 2009.
• Predicate Abstraction with Under-approximation Refinement, Corina S. Pasareanu, Radek Pelanek, Willem Visser, in Logical Methods in Computer Science, Volume 3, Issue 1, 2007.
• Finding Feasible Abstract Counter-examples, Corina S. Pasareanu, Matthew B. Dwyer, Willem Visser, in International Journal on Software Tools for Technology Transfer, November 2003, Volume 5, Number 1, 34-48.

PhD Thesis: Abstraction and Modular Reasoning for the Verification of Software.
Here is a list of my publications. See also DBLP.

International Summer School Marktoberdorf, Germany.
Old Bucharest.