Thanks for the references - I'll look into them, I'm definitely interested in multi-tool workflows given my experience (systems programmers aren't necessarily mathematicians). If only the systems programmer could be pointed at tools that don't have horrible false positive rates ... ;)
On that note, have you or anyone else you've known gotten to use Astree Analyzer? Ive been wanting to hear from field users if it's as good as they claim on bug elimination and false positives.