FXplorer: Exploration of Computed Software Behavior - A New Approach to Understanding and Verification

The craft of software understanding and verification can benefit from technologies that enable evolution toward a true engineering discipline. In current practice, software developers lack practical means to determine the full functional behavior of programs under development, and even the most thorough testing can provide only partial knowledge of behaviors. Thus, an effective technology for revealing software behaviors could have a positive impact on software understanding. This paper describes the emerging technology of function extraction (FX) for computing the functional behavior of programs and how the knowledge of program behavior can be used in user-directed program exploration for understanding and verification. We explore how the use of FX technologies can transform methods for functional verification of software. Several examples are presented illustrating the FXplorer interface and its use in exploring the behavior of programs, a capability that, without function extraction technology, has not been possible until now.