I am a research scientist 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. 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

Program chair for SPIN'09 (deadline: March 9, 2009), NFM'09 (deadline: January 30, 2009).

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,VAMP'09, FMICS'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 (reviewer 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).

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

• 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.
• Assume Guarantee Verification for Interface Automata, M. Emmi, D. Giannakopoulou, C. S. Pasareanu, in FM'08.

PhD Thesis: Abstraction and Modular Reasoning for the Verification of Software.

A comprehensive list of my publications can be found here.

International Summer School Marktoberdorf, Germany.
Old Bucharest.