Filter Based Analysis Papers
Software developers attempt to assess the quality of their designs and implementations throughout the development process. It is common-practice to test individual software units in isolation as they become available. We intend to support the application of finite-state verification techniques to individual software units as well. To achieve this one must define a verification harness (like a test harness) that establishes the environment in which the unit will execute and exercises that unit to expose defects or assess functionality.
- 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.
- 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.
- 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.
- 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.