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

Program chair for SPIN'09 (deadline: March 24, 2009), co-chair for NFM'09. Lectures at UC Berkeley.

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); the IET Software journal (special issue on Automated Compositional Verification: Techniques, Applications and Empirical Studies); the Science of Computer Programming journal.

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.