I am a research scientist at NASA Ames, in the Robust Software Engineering group. I am employed by Perot Systems Government Services. 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 co-chair for FACS'08 (deadline: May 9, 2008). 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, AFM'08 (deadline: May 25, 2008), ICCP'08 (deadline: May 1, 2008), 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

• Differential Symbolic Execution, S. Person, M. Dwyer, S. Elbaum, C. S. Pasareanu, to appear 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, to appear in ISSTA'08.
• Automated Assume-Guarantee Reasoning by Abstraction Refinement, M. Gheorghiu Bobaru, C. S. Pasareanu, D. Giannakopoulou, to appear in CAV'08.
• Assume Guarantee Verification for Interface Automata, M. Emmi, D. Giannakopoulou, C. S. Pasareanu, to appear in FM'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, Springer OnlineFirst, January 2008.
• Symbolic Execution and Model Checking for Testing, Corina S. Pasareanu, Willem Visser, in Haifa Verification Conference 2007, LNCS 4899: 17-18 (HVC Award).
• Symbolic Execution with Abstraction, Saswat Anand, Corina S. Pasareanu, Willem Visser, in STTT, 2008 (to appear).
• Assume Guarantee Testing for Software Components, D. Giannakopoulou, C. Pasareanu, C. Blundell, in IET Software (invited -- under review).
• Automatic Testcase Generation for Flight Software, D. Bushnell, C. Pasareanu, R. Mackey, NASA Planetary Spacecraft Fault Management Workshop, New Orleans, 2008 (poster).

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

A list of all my publications can be found here.

Selected Presentations

• Symbolic Execution and Model Checking for Testing (HVC'07 Invited Talk).
• Learning Based Assume-Guarantee Reasoning (FACS'07 Invited Talk).
• Towards a Compositional SPIN (SPIN'06).
• Symbolic Execution with Abstract Subsumption Checking (SPIN'06).
• Concrete Model Checking with Abstract Matching and Refinement (CAV'05).
• Lifecycle Verification of the NASA Ames K9 Rover Executive (NASA Ames 2004).
• Verification of Java Programs using Symbolic Execution and Loop Invariant Generation (UC Santa Cruz and SPIN'04).
• Automated Assume-guarantee Reasoning for Component Verification (CMU and SRI 2003).
• Symbolic Execution for Model Checking and Testing (Stanford University 2003).
• Automatic Assumption Generation for Compositional Verification (Microsoft Research 2003).
• Combination of Symbolic Execution and Model Checking (CMU 2002).
• Abstraction and Modular Reasoning for the Verification of Software (Thesis Talk 2001).
• Finding Feasible Counter-examples when Model Checking Abstracted Java Programs (TACAS'01).
• Tool-supported Program Abstraction for Finite-state Verification (ICSE'01).
• Assume-Guarantee Model Checking of Software: A Comparative Case Study (SPIN'99).

International Summer School Marktoberdorf, Germany.
Old Bucharest.