Papers
This paper gives an introduction to the patterns system.
- Property Specification Patterns for Finite-state Verification, Matthew B. Dwyer, George S. Avrunin and James C. Corbett in the 2nd Workshop on Formal Methods in Software Practice, March, 1998. An abstract of this paper is also available.
This paper gives a brief overview of our updated pattern system, describes our survey of property specifications, and presents the results of the survey (extracted from the raw data that is linked below).
- Patterns in Property Specifications for Finite-state Verification, Matthew B. Dwyer, George S. Avrunin and James C. Corbett to appear in Proceedings of the 21st International Conference on Software Engineering, May, 1999. An abstract of this paper is also available.
In addition to the basic patterns, we have developed tool support for defining the atomic propositions that parameterize patterns in terms of the execution behavior of a Java program.
- 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.
This proposition definition approach, along with an implementation of an extensible specification pattern definition system, is part of the Bandera project. We are making use of the patterns in our applied FSV research. We'll be linking a variety of different resources that provide (at least) anecdotal evidence of the utility of the patterns and examples of how they can be applied.
Some papers reporting on applications of FSV that use patterns.
- Filter-based Model Checking of Partial Systems, Matthew B. Dwyer and Corina S. Pasareanu. This paper is published as KSU CIS TR 98-3 and will appear in the ACM SIGSOFT Symposium on the Foundation of Software Engineering, November, 1998. An abstract of this paper is also available.
- Model Checking Generic Container Implementations, Matthew B. Dwyer and Corina S. Pasareanu This paper is published as KSU CIS TR 98-10 and has been submitted for publication. An abstract of this paper is also available.