The Abductor Program Analyzer                      
Abductor introduced the idea of using abductive inference to discover logical preconditions for program fargments. Usually in program anlaysis, in `whole program analyses', preconditons must be manually given, and this limits the use of such analyses during code development (for incomplete programs). Abduction is one way to remove this limitation.  

Abductor approaches bare code in a way reminiscient of how a scientist approaches the natural world: it's main algorithm is a mixed deduction-induction-abduction loop which allows pre/post specifications to be obtained from procedures, as long as specs of the callers are known, and this is the basis for an interprocedural analysis algorithm for memory properties that can scale to millions of lines of code.  

The main Abductor paper is

The source code of Abductor has been released under a BSD license; see here . Note that Abductor is no longer being maintained and that this release is made available `as is'.