Intelligent Systems Division

Corina Pasareanu, Ph.D.

I am a researcher at NASA Ames, in the Robust Software Engineering group. I am employed by Carnegie Mellon University (Sillicon Valley campus). My research interests are in software verification. I am investigating the use of abstraction and symbolic execution in the context of the Java PathFinder model checker, with applications in test input generation and error detection (see Symbolic (Java) PathFinder -- a framework for symbolic execution of Java bytecode). I am also working on using learning techniques for automating assume-guarantee compositional verification. My other interests involve the design of a command execution language and the verification of the associated execution system (PLEXIL).

Events

LNCS SPIN'09 Proceedings. Program chair for SPIN'09, co-chair for NFM'09. Lectures at UC Berkeley. ICSE'09 Tutorial on Component-based Verification.

Past Events: Program co-chair for FACS'08. Chair of Haifa Verification Award Committee (HVC'08). JPF Workshop (May 1-2, 2008). JPF in Google Summer of Code 2008. ICSE'08 Tutorial on Compositional Verification.

Program committee member for: ICSE'09, FACS'09, FMICS'09, EMSOFT'09, ASE'09 (expert review panel), AFM'09, FTfJP'09, AFM'08, ICCP'08, CONCUR'08, ASE'08, SPIN'08, FSE'08, ISSTA'08, CAV'08, ICSE'08, ISEC'08, FACS'07, ICCP'07, ESEC-FSE'07, SPIN'07, BLISS'07, ISSTA'07, ASE'07 (expert review panel), CAV'06, FSE'06, ICCP'06, SAVCBS'06, SAVCBS'05, ICSE'04 Tutorials.

Associate editor for the ACM TOSEM journal. Guest editor for: the FMSD journal (special issue on Learning Techniques for Compositional Reasoning); the IET Software journal (special issue on Automated Compositional Verification: Techniques, Applications and Empirical Studies); the Science of Computer Programming journal.

Selected Publications

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.
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, C. S. Pasareanu, D. Giannakopoulou, M. Gheorghiu Bobaru, J. M. Cobleigh, H. 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.