This paper gives an introduction to the patterns system.

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).

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.

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.