When cutpoint verification is attempted for programs that include subroutine calls, some new issues arise. I'll discuss some of those issues and talk about how I address them.
My method explicitly handles both recursive and non-recursive subroutine calls in a way that seems quite natural. It also requires very little input from the user, at least for simple programs.
David Dill and I want to use annotations in the Java source code to automatically generate all or part of the ACL2 books that my method takes as input. Thus, it's important that those books be as simple as possible.
The method is still under development, but I've applied it to over a dozen small Java bytecode programs. David Hardin and I have applied it to iterative and recursive factorial programs for Rockwell Collins' AAMP7 microprocessor.
[1] J. Matthews, J S. Moore, S. Ray, and D. Vroon: A Symbolic Simulation
Approach to Assertional Program Verification, Draft, January 2005.
http://www.cs.utexas.edu/users/sandip/publications/symbolic/main.html