TITLE: Model Checking Generic Container Implementations

AUTHORS: Matthew B. Dwyer and Corina S. Pasareanu

AFFILIATIONS:
  Department of Computing and Information Sciences (1) 
  Kansas State University

ABSTRACT:
  Model checking, and other finite-state verification, techniques and tools
  have been succesfuly applied to the verification of correctness properties
  of complex hardware systems and communication protocols.
  This success has fueled the application of these techniques to a broader
  class of software systems.  To date, this work has been limited primarily
  to concurrent software whose complexity lies, primarily,
  in the large number of possible
  execution orderings of asynchronously executing program actions.
  In this paper, we apply existing model checking techniques to
  parameterizable implementations of container data structures.
  In contrast to most of the concurrent systems that have been studied
  in the model checking literature,
  the complexity of these implementations
  lies primarily in the data structures and algorithms that they implement.
  We report our experiences model checking specifications of correctness
  properties of queue, stack and priority queue data structures
  implemented in Ada.