2005

• A New Foundation For Control-Dependence and Slicing for Modern Program Structures by Venkatesh Prasad Ranganath, Torben Amtoft, Anindya Banerjee, Matthew B. Dwyer, and John Hatcliff. Accepted at European Symposium On Programming (ESOP) held as part of ETAPS 2005.
• Kaveri: Delivering Indus Java Program Slicer to Eclipse by Ganeshan Jayaraman, Venkatesh Prasad Ranganath, and John Hatcliff. Accepted at Fundamental Approaches to Software Engineering (FASE) held as part of ETAPS 2005.

2004

• Supporting Model Checking Education using BOGOR/Eclipse, August 2004.
  Matthew B. Dwyer, John Hatcliff, Robby.
  To appear in the Proceedings of the 2004 OOPSLA Workshop on Eclipse Technology eXchange (eTX/OOPSLA 2004).
  Technical Report, SAnToS-TR2004-6.
  pdf (Last updated: January 5, 2005). Software Model Checking: Theory and Practice website
• Pruning Interference and Ready Dependence for Slicing Concurrent Java Programs [ cc04.pdf ]
  Description: Venkatesh Prasad Ranganath, John Hatcliff. Accepted at 13th International Conference on Compiler Construction (CC) 2004 held as part of ETAPS 2004. Last updated: January 9, 2004.
• Checking Strong Specifications Using An Extensible Software Model Checking Framework, April 2004.
  Robby, Edwin Rodríguez, Matthew B. Dwyer, John Hatcliff.
  In the Proceedings of the Tenth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2004).
  Technical Report, SAnToS-TR2003-10. pdf (Last updated: February 11, 2004). BibTeX
• Checking JML Specifications Using An Extensible Software Model Checking Framework, August 2004.
  Robby, Edwin Rodríguez, Matthew Dwyer, John Hatcliff.
  Submitted for publication.
  Technical Report, SAnToS-TR2004-7.
  (Extended version of TACAS 2004 paper).
  pdf (Last updated: August 2004).
• Extending Sequential Specification Techniques for Modular Specification and Verification of Multi-Threaded Programs, December 2004.
  Edwin Rodríguez, Matthew Dwyer, Cormac Flanagan, John Hatcliff, Gary T. Leavens, Robby.
  Submitted for publication.
  Technical Report, SAnToS-TR2004-10.
  pdf (Last updated: December 2004).
  
• A Flexible Framework for the Estimation of Coverage Metrics in Explicit State Software Model Checking, June 2004.
  Edwin Rodríguez, Matthew B. Dwyer, John Hatcliff, Robby.
  In the Proceedings of the 2004 International Workshop on Construction and Analysis of Safe, Secure, and Interoperable Smart Devices (CASSIS 2004).
  Technical Report, SAnToS-TR2004-3.
  pdf (Last updated: September 25, 2004). MAnTA website
• A Case Study in Domain-customized Model Checking for Real-time Component Software, July 2004.
  Matthew Hoosier, John Hatcliff, Robby, Matthew B. Dwyer.
  To appear in the Proceedings of the 1st International Symposium on Leveraging Applications of Formal Method (ISoLA 2004)
  Technical Report, SAnToS-TR2004-4.
  pdf (Last updated: July 11, 2004). Experimental Artifacts
• Extending Sequential Specification Techniques for Modular Specification and Verification of Multi-Threaded Programs, December 2004.
  Edwin Rodríguez, Matthew B. Dwyer, Cormac Flanagan, John Hatcliff, Gary T. Leavens, Robby.
  To appear in the Proceedings of 19th European Conference on Object-Oriented Programming (ECOOP 2005).
  Technical Report, SAnToS-TR2004-10.
  pdf (Last updated: December 23, 2004). SpEx-JML website
• Bogor: An Extensible Framework for Domain-Specific Model Checking, December 2004.
  John Hatcliff, Matthew B. Dwyer, Robby.
  To appear in the Newsletter of European Association of Software Science and Technology (EASST).
  Technical Report, SAnToS-TR2004-9.
  pdf (Last updated: December 1, 2004).
• Checking JML Specifications Using An Extensible Software Model Checking Framework, August 2004.
  Robby, Edwin Rodríguez, Matthew B. Dwyer, John Hatcliff.
  To appear in the International Journal of Software Tools for Technology Transfer (STTT).
  This is an extended version of Technical Report SAnToS-TR2003-10.
  Technical Report, SAnToS-TR2004-7.
  pdf (Last updated: August 9, 2004). SpEx-JML website
• Analyzing Interaction Orderings with Model Checking, April 2004.
  Matthew B. Dwyer, Robby, Oksana Tkachuk, Willem Visser.
  In the Proceedings of the Nineteenth IEEE International Conference on Automated Software Engineering (ASE 2004).
  Technical Report, SAnToS-TR2004-1.
  pdf (Last updated: April 14, 2004). BEG website
• Checking Strong Specifications Using An Extensible Software Model Checking Framework, October 2003.
  Robby, Edwin Rodríguez, Matthew B. Dwyer, John Hatcliff.
  In the Proceedings of the Tenth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2004).
  Technical Report, SAnToS-TR2003-10.
  pdf (Last updated: February 11, 2004). SpEx-JML website
• Pruning Interference and Ready Dependence for Slicing Concurrent Java Programs. (.ps) Venkatesh Prasad Ranganath, John Hatcliff. Accepted at 13th International Conference on Compiler Construction (CC) 2004 held as part of ETAPS 2004. Last updated: January 9, 2004.

2003

• Model-checking Middleware-based Event-driven Real-time Embedded Software, March 2003. William Deng, Matthew B. Dwyer, John Hatcliff, Georg Jung, Robby, Gurdip Singh. pdf
• Using Static and Dynamic Escape Analysis To Enable Model Reductions in Model-Checking Concurrent Object-Oriented Programs, February 2003.
  Matthew B. Dwyer, John Hatcliff, Venkatesh R. Prasad, Robby. pdf
• From OEP to CCM en route CAD [ SAnToS-TR2003-8.pdf ]
  Description: Venkatesh Prasad Ranganath. May 2003. This report describes Boeing OEP XML configuration format along with it's counterparts in Cadena and CCM. It also suggests translation schemes to translate an OEP XML document into CCM assembly descriptor compliant d
• Space-Reduction Strategies for Model Checking Dynamic Systems, May 2003 [ SAnToS-TR2003-1.pdf ]
  Description: Robby, Matthew B.Dwyer, John Hatcliff, Radu Iosif May 2003, Technical Report, SAnToS-TR2003-5 (Submitted for publication). Last updated: May 14, 2003.
• Bogor: An Extensible and Highly Modular Software Model Checking Framework [ SAnToS-TR2003-3.pdf ]
  Description: Robby, Matthew B. Dwyer, and John Hatcliff. March 2003. To appear in the Proceedings of the Fourth Joint Meeting of the European Software Engineering Conference and ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE 2003).
• Using Static and Dynamic Escape Analysis to Enable Model Reductions in Model-Checking Concurrent Object-Oriented Programs [ SAnToS-TR2003-5.pdf ]
  Description: Matthew B. Dwyer, John Hatcliff, Venkatesh R. Prasad, Robby. February 2003.
• Space Reductions for Model Checking Quasi-Cyclic Systems, April 2003 [ SAnToS-TR2003-4.pdf ]
  Description: Matthew B. Dwyer,Robby, William Deng, John Hatcliff. April 2003, Technical Report, SAnToS-TR2003-4 (Submitted for publication). Last updated: May 14, 2003.
• Model-checking Middleware-based Event-driven Real-time Embedded Software [ SAnToS-TR2003-2.pdf ]
  Description: William Deng, Matthew B. Dwyer, John Hatcliff, Georg Jung, Robby, and Gurdip Singh. March 2003. To appear in the Proceedings of the First International Symposium on Formal Methods for Components and Objects (FMCO 2002).
• Cadena: An Integrated Development, Analysis, and Verification Environment for Component-based Systems [ ICSE03-cadena.pdf ]
  Description: John Hatcliff, William Deng, Matthew Dwyer, Georg Jung, Venkatesh Prasad Ranganath. Proceedings of the 2003 International Conference on Software Engineering (ICSE 2003), Portland, Oregon, May 2003.
• CADENA: Enabling CCM-based Application Development in Eclipse [ eTX03.pdf ]
  Description: Venkatesh Prasad Ranganath, Adam Childs, Jesse Greenwald, Matthew B. Dwyer, John Hatcliff, Gurdip Singh. This paper has been accepted for the eclipse Technology eXchange (eTX) Workshop at OOPSLA 2003, Anaheim, California, 2003.
• Honing the Detection of Interference and Ready Dependence for Slicing Concurrent Java Programs [ SAnToS-TR2003-6.pdf ]
  Description: Venkatesh Prasad Ranganath, John Hatcliff. July 2003, Technical Report, SAnToS -TR2003-6. Last updated: October 6, 2003.
• Cadena: An Integrated Development, Analysis, and Verification Environment for Component-based Systems, John Hatcliff, William Deng, Matthew Dwyer, Georg Jung, Venkatesh Prasad Proceedings of the 2003 International Conference on Software Engineering (ICSE 2003), Portland, Oregon, May 2003.
• Honing the Detection of Interference and Ready Dependence for Slicing Concurrent Java Programs. Venkatesh Prasad Ranganath, John Hatcliff. July 2003, Technical Report, SAnToS-TR2003-6. Last updated: July 14, 2003.
• Space-Reduction Strategies for Model Checking Dynamic Systems, May 2003.
  Robby, Matthew B. Dwyer, John Hatcliff, Radu Iosif.
  To appear in the Proceedings of 2003 Workshop on Software Model Checking (SoftMC 2003).
  Technical Report, SAnToS-TR2003-5.
  pdf (Last updated: June 24, 2003).
• Space-Reduction Strategies for Model Checking Dynamic Systems, May 2003.
  Robby, Matthew B. Dwyer, John Hatcliff, Radu Iosif.
  To appear in the Proceedings of 2003 Workshop on Software Model Checking (SoftMC 2003).
  Technical Report, SAnToS-TR2003-5.
  pdf (Last updated: June 24, 2003).
• Space Reductions for Model Checking Quasi-Cyclic Systems, April 2003.
  Matthew B. Dwyer, Robby, William Deng, John Hatcliff.
  To appear in the Proceedings of the Third International Conference on Embedded Software (EMSOFT 2003).
  Technical Report, SAnToS-TR2003-4.
  pdf (Last updated: May 14, 2003). case-studies
• Bogor: An Extensible and Highly-Modular Model Checking Framework, March 2003.
  Robby, Matthew B. Dwyer, John Hatcliff
  To appear in the Proceedings of the Fourth Joint Meeting of the European Software Engineering Conference and ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE 2003).
  Technical Report, SAnToS-TR2003-3.
  pdf (Last updated: July 1, 2003).
• CADENA: Enabling CCM-based Application Development in Eclipse, Venkatesh Prasad Ranganath, Adam Childs, Jesse Greenwald, Matthew B. Dwyer, John Hatcliff, Gurdip Singh.
  
  This paper has been accepted for the eclipse Technology eXchange (eTX) Workshop at OOPSLA 2003, Anaheim, California, 2003.
• From OEP to CCM en route CAD, Venkatesh Prasad Ranganath. May 2003, Technical Report, SAnToS-TR2003-7. Last updated: July 10, 2003.
  
  This report describes Boeing OEP XML configuration format along with it's counterparts in Cadena and CCM. It also suggests translation schemes to translate an OEP XML document into CCM assembly descriptor compliant document.
• Cadena: An Integrated Development, Analysis, and Verification Environment for Component-based Systems, John Hatcliff, William Deng, Matthew Dwyer, Georg Jung, Venkatesh Prasad Ranganath. Proceedings of the 2003 International Conference on Software Engineering (ICSE 2003), Portland, Oregon, May 2003.
  
  This paper gives a condensed overview of the various capabilities of Cadena. It includes material on Cadena's dependency analysis and only a brief overview of its model-checking capabilities based on a translation to dSpin.
• Model-checking Middleware-based Event-driven Real-time Embedded Software. William Deng, Matthew Dwyer, John Hatcliff, Georg Jung, Robby, Gurdip Singh . SAnToS Technical Report SAnToS-TR2003-2. April 9, 2003.
  
  This paper covers the model-checking of Cadena in greater detail, including a description of the use of our Bogor model-checker and a detailed description of the modeling of a real-time CORBA event service.
• Verifying Atomicity Specifications for Concurrent Object-Oriented Software using Model Checking, August 2003.
  John Hatcliff, Robby, Matthew B. Dwyer.
  In the Proceedings of the Fifth International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI 2004).
  Technical Report, SAnToS-TR2003-7.
  pdf (Last updated: November 11, 2003). examples
• Space-Reduction Strategies for Model Checking Dynamic Systems, May 2003.
  Robby, Matthew B. Dwyer, John Hatcliff, Radu Iosif.
  In the Proceedings of 2003 Workshop on Software Model Checking (SoftMC 2003).
  Technical Report, SAnToS-TR2003-5.
  pdf (Last updated: August 7, 2003).
• Space Reductions for Model Checking Quasi-Cyclic Systems, April 2003.
  Matthew B. Dwyer, Robby, William Deng, John Hatcliff.
  In the Proceedings of the Third International Conference on Embedded Software (EMSOFT 2003).
  Technical Report, SAnToS-TR2003-4.
  pdf (Last updated: July 28, 2003). case-studies
• Bogor: An Extensible and Highly-Modular Model Checking Framework, March 2003.
  Robby, Matthew B. Dwyer, John Hatcliff
  In the Proceedings of the Fourth Joint Meeting of the European Software Engineering Conference and ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE 2003).
  Technical Report, SAnToS-TR2003-3.
  pdf (Last updated: July 1, 2003).
• Model-checking Middleware-based Event-driven Real-time Embedded Software, March 2003.
  William Deng, Matthew B. Dwyer, John Hatcliff, Georg Jung, Robby, Gurdip Singh.
  In the Proceedings of the First International Symposium on Formal Methods for Components and Objects (FMCO 2002).
  Technical Report, SAnToS-TR2003-2.
  pdf (Last updated: April 9, 2003).
• Exploiting Object Escape and Locking Information in Partial Order Reduction for Concurrent Object-Oriented Programs, February 2003.
  Matthew B. Dwyer, John Hatcliff, Robby, Venkatesh R. Prasad.
  In Formal Methods in System Design Journal (FMSD), Volume 25, Issue 2-3, Sep-Nov 2004, p.199-240.
  Technical Report, SAnToS-TR2003-1.
  pdf (Last updated: March 23, 2004).
  Kluwer Online (most recent)
• Honing the Detection of Interference and Ready Dependence for Slicing Concurrent Java Programs. Venkatesh Prasad Ranganath, John Hatcliff. July 2003, Technical Report, SAnToS -TR2003-6. Last updated: July 14, 2003.

2002

• Region Synchronization in Message Passing Systems [ 01040883.pdf ]
  Description: G. Singh and Ye Su, 31st International Conference on Parallel Processing, Vancouver, August 2002.

2001

• Tool-supported Program Abstraction for Finite-state Verification [ bandera-abs.pdf ]
  Description: Matthew Dwyer, John Hatcliff, Roby Joehanes, Shawn Laubach, Corina Pasareanu, Robby, Willem Visser, Hongjun Zheng, in Proceedings of the 23rd International Conference on Software Engineering, May, 2001.
• Finding Feasible Counter-examples when Model Checking Java Programs [ choosefree.pdf ]
  Description: 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.
• A Flexible Real-time Transport Protocol for Controller area Networks [ pdpta01.pdf ]
  Description: Mitch Neilsen, Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications, pp. 250-256, June 25-28, 2001.
• Tool-supported Program Abstraction for Finite-state Verification, Matthew Dwyer, John Hatcliff, Roby Joehanes, Shawn Laubach, Corina Pasareanu, Robby, Willem Visser, Hongjun Zheng, in Proceedings of the 23rd International Conference on Software Engineering, May, 2001. (to appear).
• Finding Feasible Counter-examples when Model Checking 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.

2000

• DEOS Kernel: Environment Modeling using LTL Assumptions, Corina S. Pasareanu, NASA Ames Technical Report NASA-ARC-IC-2000-196, July 2000.
• Model Checking Generic Container Implementations, Matthew B. Dwyer and Corina S. Pasareanu in Generic Programming : Proceedings of Dagstuhl Seminar, Lecture Notes in Computer Science 1766, 2000.
• A Language Framework For Expressing Checkable Properties of Dynamic Software, James C. Corbett, Matthew B. Dwyer, John Hatcliff, and Robby in Proceedings of the SPIN Software Model Checking Workshop, Lecture Notes in Computer Science, Springer-Verlag, Aug, 2000.
• A Language Framework For Expressing Checkable Properties of Dynamic Software [ SPIN00.pdf ]
  Description: James C. Corbett, Matthew B. Dwyer, John Hatcliff, and Robby in Proceedings of the SPIN Software Model Checking Workshop, Lecture Notes in Computer Science, Springer-Verlag, Aug, 2000.
• Model Checking Generic Container Implementations [ containermc.pdf ]
  Description: Matthew B. Dwyer and Corina S. Pasareanu in Generic Programming : Proceedings of Dagstuhl Seminar, Lecture Notes in Computer Science 1766, 2000.
• DEOS Kernel: Environment Modeling using LTL Assumptions [ DEOS-Env-Modeling.ps ]
  Description: Corina S. Pasareanu, NASA Ames Technical Report NASA-ARC-IC-2000-196, July 2000.

1999

• Assume-Guarantee Model Checking of Software : A Comparative Case Study, Corina S. Pasareanu, Matthew B. Dwyer and Michael Huth, in Theoretical and Practical Aspects of SPIN Model Checking, Lecture Notes in Computer Science 1680, Springer-Verlag, Sept, 1999.
• Slicing Software for Model Construction (June 1999), Matthew B. Dwyer, John Hatcliff, Hongjun Zheng, To appear in a special issue of the Journal of Higher-order and Symbolic Computation dedicated to selected papers from the 1999 ACM SIGPLAN Partial Evaluation and Program Manipulation, January, 1999.
• A Formal Study of Slicing for Multi-threaded Programs with JVM Concurrency Primitives, John Hatcliff, James C. Corbett, Matthew B. Dwyer, Stefan Sokolowski, and Hognjun Zheng, in Proceedings on the 1999 International Symposium on Static Analysis, Lecture Notes in Computer Science 1694, Sept, 1999.
• Slicing Software for Model Construction [ hosc-pepm99.ps.gz ]
  Description: Matthew B. Dwyer, John Hatcliff, Hongjun Zheng, To appear in a special issue of the Journal of Higher-order and Symbolic Computation dedicated to selected papers from the 1999 ACM SIGPLAN Partial Evaluation and Program Manipulation, January, 1999.
• A Formal Study of Slicing for Multi-threaded Programs with JVM Concurrency Primitives [ SAS99.pdf ]
  Description: John Hatcliff, James C. Corbett, Matthew B. Dwyer, Stefan Sokolowski, and Hognjun Zheng, in Proceedings on the 1999 International Symposium on Static Analysis, Lecture Notes in Computer Science 1694, Sept, 1999.
• Assume-Guarantee Model Checking of Software : A Comparative Case Study [ SPIN99.pdf ]
  Description: Corina S. Pasareanu, Matthew B. Dwyer and Michael Huth, in Theoretical and Practical Aspects of SPIN Model Checking, Lecture Notes in Computer Science 1680, Springer-Verlag, Sept, 1999.

1998

• Filter-based Model Checking of Partial Systems, Matthew B. Dwyer and Corina S. Pasareanu. in the Proceedings of the ACM SIGSOFT Sixth International Symposium on the Foundation of Software Engineering, November, 1998.
• Data-flow analysis is model checking of abstract interpretations. David A. Schmidt. Proc. 25th ACM Symp. Principles of Programming Languages, San Diego, 1998.
• Data-flow analysis as model checking of abstract interpretations. David A. Schmidt and Bernhard Steffen Invited tutorial paper, Proc. 5th Static Analysis Symposium, G. Levi. ed., Pisa, September, 1998. Springer LNCS 1503.
• Staging Static Analyses Using Abstraction-based Program Specialization , John Hatcliff, Matthew B. Dwyer, Shawn Laubach. 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.
• Data-flow analysis as model checking of abstract interpretations [ paperneu9.ps.Z ]
  Description: David A. Schmidt and Bernhard Steffen Invited tutorial paper, Proc. 5th Static Analysis Symposium, G. Levi. ed., Pisa, September, 1998. Springer LNCS 1503.
• Data-flow analysis is model checking of abstract interpretations [ dfa.ps.Z ]
  Description: David A. Schmidt. Proc. 25th ACM Symp. Principles of Programming Languages, San Diego, 1998.
• Filter-based Model Checking of Partial Systems [ mcfb.pdf ]
  Description: Matthew B. Dwyer and Corina S. Pasareanu. in the Proceedings of the ACM SIGSOFT Sixth International Symposium on the Foundation of Software Engineering, November, 1998.
• Staging Static Analyses Using Abstraction-based Program Specialization [ PLILP98-full.ps.gz ]
  Description: John Hatcliff, Matthew B. Dwyer, Shawn Laubach. 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.

Misc

• Translating Ada Programs for Model Checking : A Tutorial [ ada2model.ps ]
  Description: Matthew B.Dwyer, James C. Corbett and Corina S. Pasareanu.
• Slicing Multi-threaded Java Programs : A Case Study [ slicestudy.pdf ]
  Description: Matthew B. Dwyer, James C. Corbett, John Hatcliff, Stefan Sokolowski, and Hognjun Zheng.
• Robby's MS thesis describing the Bandera specification language in detail. [ bsl-thesis.ps.gz ]
  Description: Robby's MS thesis
• Using Partial Evaluation to Enable Verification of Concurrent Software [ pefsv.pdf ]
  Description: Matthew B. Dwyer, John Hatcliff, and Muhammad Nanda This paper is published as KSU CIS TR 97-15 and will appear in ACM Computing Surveys.
• Specializing Configurable Systems for Finite-state Verification [ ssfv.pdf ]
  Description: John Hatcliff, Matthew B. Dwyer, Shawn Laubach, and Nanda Muhammad. This paper is published as KSU CIS TR 98-4 and has been submitted for publication.
• Modular Flow Analysis for Concurrent Software [ modular.pdf ]
  Description: Matthew B. Dwyer. in Proceedings of the 12th International Conference on Automated Software Engineering, November, 1997.
• Limiting State Explosion with Filter-Based Refinement [ filter.ps.Z ]
  Description: Matthew B. Dwyer and David A. Schmidt. in Proceedings of the ILPS'97 Workshop on Verification, Model Checking and Abstract Interpretation, October, 1997.
• A Correlation Framework for the CORBA Component Model [ TR2003-9.ps ]
  Description: Georg Jung, John Hatcliff, Venkatesh Prasad Ranganath. Georg Jung, John Hatcliff, Venkatesh Prasad Ranganath. This paper gives the formal background for introducing event correlations into Cadena, thereby making them accessible to CCM frameworks.
• A Correlation Framework for the CORBA Component Model, Georg Jung, John Hatcliff, Venkatesh Prasad Ranganath. This paper gives the formal background for introducing event correlations into Cadena, thereby making them accessible to CCM frameworks. A two phase model for the correlator is introduced to provide better means for assembling expressive, data carrying correlated events.
• Robby's MS thesis describing the Bandera specification language in detail.
• 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.
• Using Partial Evaluation to Enable Verification of Concurrent Software, Matthew B. Dwyer, John Hatcliff, and Muhammad Nanda This paper is published as KSU CIS TR 97-15 and will appear in ACM Computing Surveys. An abstract of this paper is also available.
• 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 and has been submitted for publication. An abstract of this paper is also available.
• Modular Flow Analysis for Concurrent Software, Matthew B. Dwyer. in Proceedings of the 12th International Conference on Automated Software Engineering, November, 1997. An abstract of this paper is also available.
• Limiting State Explosion with Filter-Based Refinement, Matthew B. Dwyer and David A. Schmidt. in Proceedings of the ILPS'97 Workshop on Verification, Model Checking and Abstract Interpretation, October, 1997. An abstract of this paper is also available.
• BIR Documentation
• 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.