NASA Logo, National Aeronautics and Space Administration

Corina Pasareanu, ACM Distinguished Scientist

I am doing research in software engineering at NASA Ames, in the Robust Software Engineering group. I am employed by KBR, where I am Technical Professional Leader - Data Science. I am also affiliated with Carnegie Mellon University (CMU), CMU CyLab, CMU Silicon Valley, and CMU ECE. Research interests:
  • 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 also working on planning for safe surface operations for autonomous vehicles. I am now interested in the analysis of deep neural networks. See our new project at NASA: SafeDNN
  • Security, particularly side-channel analysis and worst-case execution analysis.

Events


Awards 2018: ASE Most Influential Paper Award, ESEC/FSE Test of Time Award, ISSTA Retrospective Impact Paper Award.

ACM Distinguished Scientist (2016).

CAV Award Committee (please send your nomination!). Invited speaker for CAV'21, ICST'21, Marktoberdorf Summer School 2021, SEAMS'20, POPL/VMCAI'20 Winter school, iFM'19, ATVA'18. ICST'17 Best Paper Award. Invited speaker for LICS'17. Invited speaker for Facebook's Face TAV 2017 Symposium, London, 2017. Check out our VeriS Lab at CMU Cylab. ICSE17-MIP committee, ASE'17 Workshops Co-Chair, ESEC/FSE'18 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: FM'21, ISSTA'20, ICST'20, ESEC/FSE'18, CAV'15, ISSTA'14, PASTE'13, FACS'12, ASE'11, NFM'09, SPIN'09.

Some Program Committees: FMICS'21, ISSTA'21, ICSE'22, ESOP'21, IEEE Euro S&P'20, PLDI'20, TACAS'20, CSF'19, ASE'19, ESEC/FSE'19, CAV'19, ICSE'19, TACAS'18, 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: ESEC/FSE, 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).

Selected Publications


Recent:
  • Fast Geometric Projections for Local Robustness Certification. Aymeric Fromherz, Klas Leino, Matt Fredrikson, Bryan Parno, Corina Pasareanu ICLR'21 (Spotlight Presentation).
  • A Programmatic and Semantic Approach to Explaining and Debugging Neural Network Based Object Detectors. Edward Kim, Divya Gopinath, Corina Pasareanu, Sanjit Seshia CVPR'20.
  • HyDiff: Hybrid Differential Software Analysis within the Technical Papers-track. Yannic Noller, Corina S. Pasareanu, Marcel Böhme, Youcheng Sun, Hoang Lam Nguyen, Lars Grunske ICSE'20.
  • Assume, Guarantee or Repair. Hadar Frenkel, Orna Grumberg, Corina Pasareanu and Sarai Sheinvald TACAS'20.
  • DifFuzz: differential fuzzing for side-channel analysis. Shirin Nilizadeh, Yannic Noller, Corina S. Pasareanu ICSE'19.
  • On reliability of patch correctness assessment. Xuan-Bach D. Le, Lingfeng Bao, David Lo, Xin Xia, Shanping Li, Corina S. Pasareanu ICSE'19.
  • Property Inference for Deep Neural Networks. Divya Gopinath, Hayes Converse, Corina S. Pasareanu, Ankur Taly ASE'19.
  • Symbolic Execution for Importance Analysis and Adversarial Generation in Neural Networks. Divya Gopinath, Mengshi Zhang, Kaiyuan Wang, Burak Kadron, Corina Pasareanu and Sarfraz Khurshid ISSRE'19
  • DeepSafe: A Data-driven Approach for Checking Adversarial Robustness in Neural Networks Divya Gopinath, Guy Katz, Corina S. Pasareanu, Clark Barrett https://arxiv.org/abs/1710.00486
  • POSTER: AFL-based Fuzzing for Java with Kelinci Rody Kersten, Kasper Søe Luckow, Corina S. Pasareanu CCS 2017
  • Synthesis of Adaptive Side-Channel Attacks Quoc-Sang Phan, Lucas Bang, Corina S. Pasareanu, Pasquale Malacaria, Tevfik Bultan CSF'17
  • Symbolic Complexity Analysis Using Context-Preserving Histories Kasper Søe Luckow, Rody Kersten, Corina S. Pasareanu ICST 2017 Best Paper Award
  • Model-Counting Approaches for Nonlinear Numerical Constraints Mateus Borges, Quoc-Sang Phan, Antonio Filieri, Corina S. Pasareanu NFM'17
  • Planning, Scheduling and Monitoring for Airport Surface Operations. Robert Morris, Corina S. Pasareanu, Kasper Søe Luckow, Waqar Malik, Hang Ma, T. K. Satish Kumar, Sven Koenig AAAI Workshop: Planning for Hybrid Systems 2016.
  • String analysis for side channels with segmented oracles. Lucas Bang, Abdulbaki Aydin, Quoc-Sang Phan, Corina S. Pasareanu, Tevfik Bultan. In ESEC/FSE'16.
  • 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: Compositional Verification: Abstraction: PhD Thesis: Abstraction and Modular Reasoning for the Verification of Software.
Here is a list of my publications. See also DBLP.

Class on Software Verification and Testing at CMU SV. International Summer School Marktoberdorf, Germany. Romania's Castles.


Contact


Corina Pasareanu, Ph.D.

NASA Ames Research Center
Mail Stop 269-2
Moffett Field, CA 94035

Phone: +1 (650) 604-4767
Fax:     +1 (650) 604-3594

Email: Corina.S.Pasareanu "at" nasa.gov

First Gov logo
NASA Logo - nasa.gov