NASA Logo, National Aeronautics and Space Administration

Publications

Books/Book Chapters/Edited Volumes/Proceedings

  • 26th IEEE/ACM International Conference on Automated Software Engineering (ASE 2011 Proceedings), Perry Alexander, Corina S. Pasareanu, John G. Hosking, Lawrence, KS, USA, November 6-10, 2011 IEEE 2011.
  • Model Checking Software, 16th International SPIN Workshop, Corina S. Pasareanu, Grenoble, France, June 26-28, 2009. Proceedings Springer 2009.
  • NASA Formal Methods Proceedings, Ewen Denny, Dimitra Giannakopoulou, Corina S. Pasareanu, First Symposium, NASA Ames, 2009.
  • Special issue on learning techniques for compositional reasoning, Dimitra Giannakopoulou and Corina S. Pasareanu. Formal Methods in System Design 32(3) (2008)
  • Program Model Checking - A Practitioner's Guide, Masoud Mansouri-Samani, Peter Mehlitz, Corina S. Pasareanu, John Penix, Guillaume Brat, Lawrence Markosian, Owen O'Malley, Thomas Pressburger, and Willem Visser, NASA/TM-2008-214577, January 2008.
  • Foundations of the Bandera Abstraction Tools, John Hatcliff, Matthew B. Dwyer, Corina S. Pasareanu, Robby, in The Essence of Computation 2002: 172-203.

Journal Articles

Conference and Workshop Papers

  • Memoise: A Tool for Memoized Symbolic Execution, Guowei Yang, Sarfraz Khurshid, Corina S. Pasareanu. In ICSE 2013 Formal Demo.
  • Compositional Symbolic Execution through Program Specialization, José Miguel Rojas and Corina S. Păsăreanu. In BYTECODE'13 (ETAPS'13).
  • Reliability Analysis in Symbolic Pathfinder, Antonio Filieri, Corina S. Păsăreanu, and Willem Visser. In ICSE 2013.
  • Polyglot: Systematic Analysis for Multiple Statechart Formalisms (tool demo), Corina Pasareanu, Daniel Balasubramanian, Gabor Karsai and Michael Lowry. In TACAS 2013.
  • Symbolic Quantitative Information Flow, Quoc-Sang Phan, Pasquale Malacaria, Oksana Tkachuk and Corina S. Pasareanu. In JPF Workshop 2012.
  • Abstract Pathfinder, Artem Khyzha, Pavel Parizek and Corina Pasareanu. In JPF Workshop 2012.
  • Testing Android Apps Through Symbolic Execution, Nariman Mirzaei, Sam Malek, Corina Pasareanu, Naeem Esfahani and Riyadh Mahmood. In JPF Workshop 2012.
  • Improving Symbolic Execution for Statechart Formalisms, D. Balasubramanian, C. Pasareanu, M. Whalen, G. Karsai, M. Lowry. In MoDeVVa 2012.
  • Memoized Symbolic Execution, Guowei Yang, Corina S. Pasareanu and Sarfraz Khurshid, in ISSTA 2012.
  • Learning Probabilistic Systems from Tree Samples, Anvesh Komuravelli, Corina S. Pasareanu and Edmund M. Clarke, in LICS 2012.
  • Assume-Guarantee Abstraction Refinement for Probabilistic Systems, Anvesh Komuravelli, Corina S. Pasareanu and Edmund M. Clarke, in CAV 2012.
  • Symbolic Execution with Interval Constraint Solving and Meta-Heuristic Search, Mateus Borges, Marcelo D'Amorim, Saswat Anand, David Bushnell and Corina Pasareanu, in ICST 2012.
  • Integrating Statechart Components in Polyglot, Daniel Balasubramanian, Corina Pasareanu, Gabor Karsai, Thomas Pressburger, Michael Lowry and Jason Biatek, in NFM 2012
  • Symbolic Execution Enhanced System Testing, Misty Davies, Corina S. Pasareanu, Vishwanath Raman, in VSTTE 2012.
  • Symbolic Execution with Mixed Concrete-Symbolic Solving, C. Pasareanu, N. Rungta, W. Visser, in ISSTA'11.
  • Polyglot: Modeling and Analysis for Multiple Statechart Formalisms, D. Balasubramanian, C. Pasareanu, M. Whalen, G. Karsai, M. Lowry, in ISSTA'11.
  • CORAL: Solving Complex Constraints for Symbolic PathFinder, Matheus Souza, Mateus Borges, Marcelo d'Amorim and Corina Pasareanu, in NFM'11.
  • Symbolic Execution for Software Testing in Practice – Preliminary Assessment, C. Cadar, P. Godefroid, S. Khurshid, C. Pasareanu, K. Sen, N. Tillmann, in ICSE'11 Impact Project.
  • Interface decomposition for service compositions, D. Bianculli, D. Giannakopoulou, C. Pasareanu, in ICSE'11.
  • Symbolic Pathfinder: Symbolic Execution of Java bytecode, C. S. Pasareanu, N. Rungta , in ASE'10 (tool paper).
  • Parallel Symbolic Execution for Structural Test Generation, M. Staats, C. S. Pasareanu, in ISSTA'10.
  • Learning Component Interfaces with May and Must Abstractions, R. Singh, D. Giannakopoulou, C. Pasareanu, in CAV'10.
  • Model Based Analysis and Test Generation for Flight Software, C. S. Pasareanu, J. Schumann, P. Mehlitz, M. Lowry, G. Karasai, H. Nine, S. Neema, in SMC_IT, 2009.
  • A Test Generation Framework for Distributed Fault Tolerant Algorithms,A. Goodloe, C.S. Pasareanu, D. Bushnell, P. Miner, in AFM, 2009 (affiliated with CAV).
  • Differential Symbolic Execution, S. Person, M. Dwyer, S. Elbaum, C. S. Pasareanu, in FSE'08.
  • Tool Support for Parametric Analysis of Large Software Simulation Systems. ASE 2008: 497-498 Johann Schumann, Karen Gundy-Burlet, Corina S. Pasareanu, Tim Menzies, Tony Barrett, in ASE'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.
  • Automated Assume-Guarantee Reasoning by Abstraction Refinement, M. Gheorghiu Bobaru, C. S. Pasareanu, D. Giannakopoulou, in CAV'08.
  • Assume Guarantee Verification for Interface Automata, M. Emmi, D. Giannakopoulou, C. S. Pasareanu, in FM'08.
  • Symbolic Execution and Model Checking for Testing, Corina S. Pasareanu, Willem Visser, in Haifa Verification Conference 2007, LNCS 4899: 17-18 (HVC Award).
  • Automatic Testcase Generation for Flight Software, D. Bushnell, C. Pasareanu, R. Mackey, NASA Planetary Spacecraft Fault Management Workshop, New Orleans, 2008 (poster).
  • Formal Software Analysis: Emerging Trends in Software Model Checking (invited),Matthew B. Dwyer, John Hatcliff, Robby, Corina S. Pasareanu, Willem Visser, in ICSE'07.
  • Refining Interface Alphabets for Compositional Verification,Mihaela Gheorghiu, Dimitra Giannakopoulou, Corina S. Pasareanu, in Proceedings of TACAS'07.
  • JPF--SE: A Symbolic Execution Extension to Java PathFinder (tool description), Saswat Anand, Corina S. Pasareanu, Willem Visser, in Proceedings of TACAS'07.
  • A Formal Analysis Framework for PLEXIL, G. Dowek, C. Munoz, C. S. Pasareanu, in Proceedings of 3rd ICAPS Workshop on Planning and Plan Execution for Real-World Systems, 2007.
  • Test Input Generation for Java Containers using State Matching, Willem Visser, Corina S. Pasareanu, Radek Pelanek, in Proceedings of ISSTA'06.
  • Towards a Compositional SPIN, Corina S. Pasareanu, Dimitra Giannakopoulou, in Proceedings of SPIN'06.
  • Symbolic Execution with Abstract Subsumption Checking, Saswat Anand, Corina S. Pasareanu, Willem Visser, in Proceedings of SPIN'06.
  • Universal Executive and PLEXIL: Engine and Language for Robust Spacecraft Control and Operations, Vandi Verma, Ari Jonsson, Corina Pasareanu, Michael Iatauro, in Proceedings of SPACE'06.
  • Test Input Generation for Red Black Trees using Abstraction, Willem Visser, Corina S. Pasareanu, Radek Pelanek, in Proceedings of ASE'05.
  • Assume Guarantee Testing, Colin Blundell, Dimitra Giannakopoulou, Corina S. Pasareanu, in Proceedings of SAVCBS'05 (ESEC/FSE'05 workshop).
  • Learning-Based Assume-Guarantee Verification (tool presentation), Dimitra Giannakopoulou, Corina S. Pasareanu, in Proceedings of SPIN'05.
  • Concrete Model Checking with Abstract Matching and Refinement, Corina S. Pasareanu, Radek Pelanek, Willem Visser, in Proceedings of CAV'05.
  • Lifecycle Verification of the NASA Ames K9 Rover Executive, Dimitra Giannakopoulou, Corina S. Pasareanu, Michael Lowry, Rich Washington, in Proceedings of ICAPS'05 Workshop on Verification and Validation of Model-Based Planning and Scheduling Systems.
  • Plan Execution Interchange Language (PLEXIL) for Command Execution, Vandi Verma, Tara Estlin, Ari Jonsson, Corina S. Pasareanu, Reid Simmons, in Proceedings of iSAIRAS'05.
  • Test Input Generation in Java Pathfinder, Willem Visser, Corina S. Pasareanu, Sarfraz Khurshid, in Proceedings of the International Symposium on Software Testing and Analysis (ISSTA 2004).
  • Verification of Java Programs using Symbolic Execution and Invariant Generation, Corina S. Pasareanu, Willem Visser, in Proceedings of the the 11th International SPIN Workshop on Model Checking of Software, 2004.
  • Assume-guarantee Verification of Source Code with Design-Level Assumptions, Dimitra Giannakopoulou, Corina S. Pasareanu, Jamieson M. Cobleigh, in Proceedings of the the 26th International Conference on Software Engineering, 2004.
  • Automated Environment Generation for Software Model Checking, Oksana Tkachuk, Matthew Dwyer, Corina S. Pasareanu, in Proceedings of the 18th IEEE International Conference on Automated Software Engineering, 2003.
  • Proof Rules for Automated Compositional Verification through Learning, Howard Barringer, Dimitra Giannakopoulou, Corina S. Pasareanu, in Proceedings of the Specification and Verification of Component-Based Systems (SAVCBS'03) - workshop affiliated with ESEC/FSE 2003.
  • Generalized Symbolic Execution for Model Checking and Testing, Sarfraz Khurshid, Corina S. Pasareanu, Willem Visser, in Proceedings of the 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2003.
  • Learning Assumptions for Compositional Verification, Jamieson M. Cobleigh, Dimitra Giannakopoulou, Corina S. Pasareanu, in Proceedings of the 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2003.
  • Experimental Evaluation of Verification and Validation Tools on Martian Rover Software, Guillaume Brat, Dimitra Giannakopoulou, Allen Goldberg, Klaus Havelund, Michael Lowry, Corina S. Pasareanu, Arnaud Venet, Willem Visser, in Proceedings of the SEI Software Model Checking Workshop, Pittsburgh, 2003 (invited paper).
  • Experiments with Test Case Generation and Runtime Analysis, Cyrille Artho, Doron Drusinksy, Allen Goldberg, Klaus Havelund, Michael Lowry, Corina S. Pasareanu, Grigore Rosu, Willem Visser, in Proceedings of the 10th International Workshop on Abstract State Machines, 2003 (invited paper).
  • Assumption Generation for Software Component Verification, Dimitra Giannakopoulou, Corina S. Pasareanu, Howard Barringer, in Proceedings of the 17th IEEE International Conference on Automated Software Engineering, 2002 (won ACM SIGSOFT Distinguished Paper Award).
  • Finding Feasible Counter-examples when Model Checking Abstracted Java Programs, Corina S. Pasareanu, Matthew B. Dwyer, Willem Visser, in Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2001. (© Springer-Verlag)
  • Tool-supported Program Abstraction for Finite-state Verification, Matthew B. Dwyer, John Hatcliff, Robby Joehanes, Shawn Laubach, Corina S. Pasareanu, Robby, Willem Visser, Hongjun Zheng, in Proceedings of the 23rd International Conference on Software Engineering, 2001.
  • Bandera: Extracting Finite-state Models from Java Source Code, James C. Corbett, Matthew B. Dwyer, John Hatcliff, Shawn Laubach, Corina S. Pasareanu, Robby, Hongjun Zheng, in Proceedings of the 22nd International Conference on Software Engineering, 2000.
  • Assume-Guarantee Model Checking of Software: A Comparative Case Study, Corina S. Pasareanu, Matthew B. Dwyer, Michael Huth, in Theoretical and Practical Aspects of SPIN Model Checking, Lecture Notes in Computer Science 1680, Springer-Verlag, 1999. (© Springer-Verlag)
  • Model Checking Generic Container Implementations, Matthew B. Dwyer and Corina S. Pasareanu, in Generic Programming---Proceedings of a Dagstuhl Seminar, Volume Editors: M. Jazayeri, R. Loos, D. Musser, Lecture Notes in Computer Science 1766, Springer-Verlag.
  • Filter-based Model Checking of Partial Systems, Matthew B. Dwyer and Corina S. Pasareanu, in Proceedings of the 6th ACM SIGSOFT Symposium on the Foundations of Software Engineering, 1998.

Technical Reports


First Gov logo
NASA Logo - nasa.gov