Refereed Publications

1. Invariant-based Specification, Synthesis and Verification of Synchronization in Concurrent Programs , Xinghua Deng, Matthew B. Dwyer, John Hatcliff and Masaaki Mizuno , Proceedings of the 24th International Conference on Software Engineering, May 2002.
2. Expressing Checkable Properties of Dynamic Systems: The Bandera Specification Language , James C. Corbett, Matthew B. Dwyer, John Hatcliff, and Robby International Journal on Software Tools for Technology Transfer, to appear 2002.
3. Tool-supported Program Abstraction for Finite-state Verification , Matthew B. Dwyer, John Hatcliff, Roby Joehanes, Shawn Laubach, Corina S. Pasareanu, Robby, Willem Visser and Hongjun Zheng , Proceedings of the 23rd International Conference on Software Engineering, May 2001.
4. Finding Feasible Counter-examples when Model Checking Abstracted Java Programs, Corina S. Pasareanu, Matthew B. Dwyer and Willem Visser, Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science, Springer-Verlag, April, 2001.
5. A Language Framework For Expressing Checkable Properties of Dynamic Software, James C. Corbett, Matthew B. Dwyer, John Hatcliff, and Robby Proceedings of the SPIN Software Model Checking Workshop, Lecture Notes in Computer Science 1885, Springer-Verlag, Aug. 2000.
6. Bandera : Extracting Finite-state Models from Java Source Code, James C. Corbett, Matthew B. Dwyer, John Hatcliff, Shawn Laubach, Corina S. Pasareanu, Robby, and Hongjun Zheng Proceedings of the 22nd International Conference on Software Engineering, June 2000.
7. Slicing Software for Model Construction, John Hatcliff, Matthew B. Dwyer and Hongjun Zheng, Journal of Higher-order and Symbolic Computation, 13(4), Dec. 2000.
8. Benchmarking Finite-state Verifiers, George S. Avrunin, James C. Corbett and Matthew B. Dwyer, International Journal on Software Tools for Technology Transfer, 2(4), 317-320, April 2000.
9. Model Checking Generic Container Implementations, Matthew B. Dwyer and Corina S. Pasareanu Generic Programming -- International Seminar on Generic Programming, Dagstuhl Castle, April 27-May 1, 1998, Selected Papers, Lecture Notes in Computer Science 1766, Springer-Verlag, 2000.
10. A Formal Study of Slicing for Multi-threaded Programs with JVM Concurrency Primitives, John Hatcliff, James C. Corbett, Matthew B. Dwyer, Stefan Sokolowski, and Hongjun Zheng, Proceedings of the Sixth International Static Analysis Symposium, Lecture Notes in Computer Science 1694, Springer-Verlag, Sept. 1999.
11. Assume-Guarantee Model Checking of Software : A Comparative Case Study, Corina S. Pasareanu, Matthew B. Dwyer and Michael Huth, Theoretical and Practical Aspects of SPIN Model Checking, Lecture Notes in Computer Science 1680, Springer-Verlag, Sept. 1999.
12. Patterns in Property Specifications for Finite-state Verification , Matthew B. Dwyer, George S. Avrunin, and James C. Corbett. Proceedings of the 21st International Conference on Software Engineering, May 1999.
13. Slicing Software for Model Construction , Matthew B. Dwyer and John Hatcliff, Proceedings of ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation (PEPM'99), January 1999.
14. Filter-based Model Checking of Partial Systems, Matthew B. Dwyer and Corina S. Pasareanu. Proceedings of the ACM SIGSOFT Sixth International Symposium on the Foundation of Software Engineering, November 1998.
15. Staging Static Analyses Using Abstraction-based Program Specialization , John Hatcliff, Matthew B. Dwyer, Shawn Laubach, and David Schmidt. This paper is published as KSU CIS TR 98-5 and a more compact version appeared in LNCS 1490 (Principles of Declarative Programming: 10th International Symposium, PLILP'98), September, 1998.
16. Using Partial Evaluation to Enable Verification of Concurrent Software, Matthew B. Dwyer, John Hatcliff, and Muhammad Nanda, ACM Computing Surveys 30(3es), Sept. 1998.
17. Property Specification Patterns for Finite-state Verification, Matthew B. Dwyer, George S. Avrunin and James C. Corbett Proceedings of the 2nd Workshop on Formal Methods in Software Practice, March 1998.
18. A Framework for Parallel Adaptive Grid Simulations, Matthew B. Dwyer and Virgil Wallentine. Concurrency : Practice and Experience, 9(11), pp. 1293-1310, Nov. 1997.
19. Modular Flow Analysis for Concurrent Software, Matthew B. Dwyer. Proceedings of the 12th International Conference on Automated Software Engineering, November 1997.
20. Limiting State Explosion with Filter-Based Refinement, Matthew B. Dwyer and David A. Schmidt. Proceedings of the ILPS'97 Workshop on Verification, Model Checking and Abstract Interpretation, October 1997.
21. Model Checking Graphical User Interfaces Using Abstractions, Matthew B. Dwyer, Vicki Carr and Laura Hines. Proceedings of the 6th European Software Engineering Conference together with 5th ACM SIGSOFT Symposium on the Foundation of Software Engineering, Lecture Notes in Computer Science 1301, Springer-Verlag, September 1997.
22. Object-Oriented Coordination Abstractions for Parallel Software, Matthew B. Dwyer and Virgil Wallentine. Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications (PDPTA'97), June 1997.
23. Gaining Confidence in Distributed Systems, Gleb Naumovich, Lori A. Clarke, Leon J. Osterweil, and Matthew B. Dwyer, Proceedings of the Tenth International Software Quality Week, Vol II, Session 10, San Francisco, CA, May 1997.
24. An Application-Independent Concurrency Skeleton in Ada-95, Matthew B. Dwyer, Matthew J. Craig, and Eric Runquist. Proceedings of the TRI-Ada'96 Conference, Philadelphia, PA, December 1996.
25. A Compact Petri Net Representation and Its Implications for Analysis, Matthew B. Dwyer and Lori A. Clarke, IEEE Transactions on Software Engineering, 22(11), November 1996.
26. A Flexible Architecture for Building Data Flow Analyzers, Matthew B. Dwyer and Lori A. Clarke, Proceedings of the Eighteenth International Conference on Software Engineering, Berlin, Germany, March 1996.
27. A Compact Petri Net Representation for Concurrent Programs, Matthew B. Dwyer, Lori A. Clarke, and Kari A. Nies , Proceedings of the Seventeenth International Conference on Software Engineering, Seattle , WA, April 1995, pp. 147-157.
28. Data Flow Analysis for Verifying Properties of Concurrent Programs, Matthew B. Dwyer and Lori A. Clarke, Proceedings of the Second ACM SIGSOFT Symposium on Foundations of Software Engineering, New Orleans, LA, December 1994, pp. 62-75.

Books and Edited Volumes

• Model Checking Software, Matthew B. Dwyer (Editor), Proceedings of the 8th SPIN Workshop on Model Checking of Software, LNCS 2057, May, 2001.

Submitted for Publication

• Comparing Finite-State Verification Techniques for Concurrent Software, George S. Avrunin, James C. Corbett, Matthew B. Dwyer, Corina S. Pasareanu, and Stephen F. Siegel. This paper is being significantly revised, but will be done in the Spring of 2002.
• Flow Analysis for Verifying Specifications of Concurrent and Distributed Software, Matthew B. Dwyer, Lori A. Clarke, Jamieson Cobleigh, and Gleb Naumovich. This paper is being significantly revised, but will be done in the Spring of 2002.

Reviewed (but not formally refereed) Publications

• Using the Bandera Tool Set to Model-check Properties of Concurrent Java Software (invited tutorial), John Hatcliff and Matthew B. Dwyer , Proceedings of CONCUR 2001 - the 13th International Conference on Concurrency Theory, Lecture Notes in Computer Science, Springer-Verlag, August, 2001.
• Bandera: A Source-level Interface for Model Checking Java Programs, James C. Corbett, Matthew B. Dwyer, John Hatcliff, and Robby, to appear in Proceedings of the 22nd International Conference on Software Engineering, June, 2000.
• Bandera: Tools for Automated Reasoning about Software System Behaviour, Matthew B. Dwyer, John Hatcliff, and Dave Schmidt, is published in ERCIM News, No. 36, January, 1999.
• Automated Analysis of Software Frameworks, Matthew B. Dwyer. position paper for ESEC/FSE'97 Workshop on Foundations of Component-Based Systems, September, 1997.
• Verification of Concurrent Software with FLAVERS, Gleb Naumovich, Lori A. Clarke, Leon J. Osterweil, and Matthew B. Dwyer, in the Proceedings of the 19th International Conference on Software Engineering, May, 1997.

Unreviewed Publications and Technical Reports

• Slicing Multi-threaded Java Programs : A Case Study, Matthew B. Dwyer, James C. Corbett, John Hatcliff, Stefan Sokolowski, and Hognjun Zheng, This paper is published as KSU CIS TR 99-7.
• Practical Parallelization : Experience with a Complex Flow Analysis, Matthew B. Dwyer and Matthias Martin. This paper is published as KSU CIS TR 99-4.
• Translating Ada Programs for Model Checking : A Tutorial, Matthew B. Dwyer, James C. Corbett and Corina S. Pasareanu. This paper is published as KSU CIS TR 98-12. An online version of this paper (with additional resources linked) is available here.
• Specializing Configurable Systems for Finite-state Verification, John Hatcliff, Matthew B. Dwyer, Shawn Laubach, and Nanda Muhammad. This paper is published as KSU CIS TR 98-4.
• Logical Support for High-Assurance Software Evolution, Matthew B. Dwyer, Brian Howard, David A. Schmidt, and Allen Stoughton Software Engineering Notes, 22(5), pp 48, September, 1997.
• High-Level Coordination Abstractions in Stock Languages, Matthew B. Dwyer and Matthew J. Craig. This paper is published as KSU CIS TR 96-9.
• Data Flow Analysis Frameworks for Concurrent Programs, Matthew B. Dwyer. This paper is published as KSU CIS TR 95-8. An alternate version of this work is described in an extended abstract.
• Data Flow Analysis for Verifying Correctness Properties of Concurrent Programs, Matthew B. Dwyer, Phd Dissertation, University of Massachusetts, Amherst, MA, September 1995.