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 ahve
a positive impact on software understanding. This paper describes the
emerging technology of functional extraction (FX) for computing the
full behavior of programs and how the knowledge of program behavior
can be used in user-directed program exploration for code understanding
and verification. We explore how the user of FX technologies can
transform methods for function 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.