I am doing research in software engineering at NASA Ames, in the Robust Software
. I am employed by Carnegie Mellon University
, at the Silicon Valley campus
I am affiliated with CMU CyLab
and also hold a courtesy appointment with CMU ECE
- Model checking and automated testing: I investigate the use of abstraction and symbolic execution
in the context of Java PathFinder, with applications to test input generation and error
detection. Together with many collaborators, I have developed Symbolic PathFinder (SPF, jpf-symbc), a symbolic execution tool for Java bytecode.
See NASA article on the use of SPF in industry.
- Compositional verification: I also work on using learning and abstraction techniques for automating assume-guarantee style compositional verification.
Recently I have worked on compositional techniques for probabilistic systems and I am currently investigating hybrid systems.
- Model-based development: Together with collaborators from Vanderbilt University and University of Minnesota, we have developed modeling and analysis techniques for multiple statechart formalisms used in the development of NASA systems. See the Polyglot tool-set.
- Probabilistic software analysis: Recently I have started to investigate probabilistic techniques for the analysis of software components placed in stochastic environments. See project webpage.
- Autonomy: I was part of the core team that developed PLEXIL, a plan execution language and system for automation. I am now interested in planning for safe surface operations for autonomous vehicles.
- Security: I am a principal investigator on the ISSTAC project -- Integrated Symbolic Execution for Space-Time Analysis of Code.
Future: ICSE17-MIP committee, ASE17 Workshops Co-Chair, FSE18 Program Co-Chair.
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.
General or Program Chair for: CAV 2015, ISSTA 2014, PASTE 2013, FACS 2012, ASE 2011, NFM 2009, SPIN 2009.
Some Program Committees: ICSE'18, CAV'17, ICSE-NIER'17, ICSE'17, ECOOP'17, ISSTA'17, ICST'17, SPIN'17, VMACAI'17, ISEC'17, FORTE'17, CAV'16, ASE'16, POPL'16, TACAS'16, ICSE'16, ISEC'16, FSE'16.
Associate editor for IEEE TSE (current), ACM TOSEM (past). Steering Committees: ISSTA and FACS.
Invited talk at VSSE'13 (ETAPS'13) on "Memoized Symbolic Execution". Lectures at International Summer School Marktoberdorf, Germany, 2012. Lectures at SRI Formal Methods school, 2012. Keynote Speaker at Test & Proof TAP'12.
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).
- Multi-run side-channel analysis using Symbolic Execution and Max-SMT. Corina Pasareanu, Quoc-Sang Phan, Pasquale Malacaria. In CSF 2016.
- Automated Circular Assume-Guarantee Reasoning with N-way Decomposition and Alphabet Refinement. Karam Abd Elkader, Orna Grumberg, Corina S. Pasareanu, Sharon Shoham. In CAV 2016.
- Automated Circular Assume-Guarantee Reasoning. Karam Abd Elkader, Orna Grumberg, Corina S. Pasareanu, Sharon Shoham. In FM 2015. (invited for journal submission)
- Compositional Symbolic Execution with Memoized Replay. Rui Qiu, Guowei Yang, Corina S. Pasareanu, Sarfraz Khurshid. in ICSE 2015.
- Iterative distribution-aware sampling for probabilistic symbolic execution. Mateus Borges, Antonio Filieri, Marcelo d'Amorim, Corina S. Pasareanu.In ESEC/SIGSOFT FSE 2015.
- Compositional Solution Space Quantification for Probabilistic Software Analysis. Mateus Borges, Antonio Filieri, Marcelo D'Amorim, Corina S. Pasareanu, Willem Visser. In PLDI 2014.
- Statistical Symbolic Execution with Informed Sampling, Antonio Filieri, Corina S. Păsăreanu, Willem Visser, and Jaco Geldenhuys. In FSE 2014.
- Exact and Approximate Probabilistic Symbolic Execution for Nondeterministic Programs, Kasper Luckow, Corina S. Pasareanu, Matt Dwyer, Antonio Filieri, Willem Visser. In ASE 2014.
- Quantifying Information Leaks using Reliability Analysis, Quoc-Sang Phan, Pasquale Malacaria, Corina Pasareanu and Marcelo D'Amorim. In SPIN 2014.
- Assume-Guarantee Abstraction Refinement Meets Hybrid Systems, Sergiy Bogomolov, Goran Frehse, Marius Greitschus, Radu Grosu, Corina Pasareanu, Andreas Podelski and Thomas Strump. In HVC 2014 (best paper award).
- Reliability analysis in symbolic pathfinder. Antonio Filieri, Corina S. Pasareanu, Willem Visser.In ICSE 2013.
- Assume-Guarantee Abstraction Refinement for Probabilistic Systems. Anvesh Komuravelli, Corina S. Pasareanu, Edmund M. Clarke. In CAV 2012.
- Learning Probabilistic Systems from Tree Samples. Anvesh Komuravelli, Corina S. Pasareanu, Edmund M. Clarke. In LICS 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).
- 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.
PhD Thesis: Abstraction and Modular Reasoning for the Verification of
- 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.
is a list of my publications. See also DBLP.
Class on Software Verification and Testing
at CMU SV.
International Summer School Marktoberdorf