TITLE: Specializing Configurable Software for Finite-state Verification

AUTHORS: John Hatcliff (1), Matthew B. Dwyer (1), Shawn Laubach (1), 
         Jason Mayans (2) and Nanda Muhammad (2)

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

  Department of Computer Science (2)
  Oklahoma State University

ABSTRACT:
  As finite-state verification techniques and tools, such as model checkers,
  continue to mature, researchers and practitioners attempt
  to apply them in increasingly realistic software development settings.
  Concurrent applications, and components of those applications, 
  are often implemented as configurable systems, i.e., where size, structure
  or selected behavior aspects are taken as system inputs.
  These systems are typically implemented using dynamically allocated
  data and threads of control.
  This use of dynamism makes it very difficult to render 
  behavioral models of configurable systems that would
  be suitable as input to finite-state verification tools.

  Currently, configurable systems can
  only be verified by performing hand-transformations of the source code
  that are often time-consuming, tedious, and error-prone.  
  In this paper, we apply
  partial evaluation techniques to transform source code automatically
  into a form from which finite-state systems can be extracted.  We
  illustrate these techniques by transforming a real configurable
  software system to a form that can be input to existing finite-state
  verification tools.  This demonstrates one way that 
  partial evaluation technology
  has the potential to significantly extend the applicability of 
  finite-state verification tools for software systems.