Publications

Book Chapter

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

Predicate Abstraction with Underapproximation Refinement, Corina S. Pasareanu, Radek Pelanek, Willem Visser, in Logical Methods in Computer Science, Volume 3, Issue 1, 2007.
Combining Test Case Generation and Runtime Verification, Cyrille Artho, Howard Barringer, Allen Goldberg, Klaus Havelund, Sarfraz Khurshid, Michael Lowry, Corina S. Pasareanu, Grigore Rosu, Koushik Sen, Willem Visser, Rich Washington, special issue "Abstract State Machines and High-Level System Design and Analysis" , Vol. 336-2/3 of the journal Theoretical Computer Science, 2005.
Component Verification with Automatically Generated Assumptions, Dimitra Giannakopoulou, Corina S. Pasareanu, Howard Barringer, in International Journal on Automated Software Engineering (2005), 12(3):297-320.
Verifying Time Partitioning in the DEOS Scheduling Kernel, John Penix, Willem Visser, SeungJoon Park, Corina S. Pasareanu, Eric Engstrom, Aaron Larson, Nicholas Weininger, in International Journal on Formal Methods in System Design, 2005, 26(2):103-135.
Experimental Evaluation of Verification and Validation Tools on Martian Rover Software, Guillaume Brat, Dimitra Giannakopoulou, Allen Goldberg, Klaus Havelund, Mike Lowry, Corina S. Pasareanu, Arnaud Venet, Willem Visser, Rich Washington, in International Journal on Formal Methods in System Design, September - November 2004, Volume 25, Issue 2-3, 167-198.
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.

Conference and Workshop Papers

Formal Software Analysis: Emerging Trends in Software Model Checking (invited), Matthew B. Dwyer, John Hatcliff, Robby, Corina S. Pasareanu, Willem Visser, in Proceedings of 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 Robust 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

Abstraction and Assume-guarantee Reasoning for Automated Software Verification, S. Chaki, E. Clarke, D. Giannakopoulou, C. Pasareanu, RIACS Technical Report, 2004.
DEOS Kernel: Environment Modeling using LTL Assumptions, Corina S. Pasareanu, NASA Ames Technical Report NASA-ARC-IC-2000-196, 2000.
Comparing Finite-State Verification Techniques for Concurrent Software, George S. Avrunin, James C. Corbett, Matthew B. Dwyer, Corina S. Pasareanu, Stephen F. Siegel, Technical Report UM-CS-1999-069, Department of Computer Science, University of Massachusetts, 1999.
Translating Ada Programs for Model Checking : A Tutorial, Matthew B. Dwyer, James C. Corbett, Corina S. Pasareanu, Technical Report KSU-CIS-TR-98-12, 1998.