During Daedalus project, PolySpace has developped PolySpace Verifier, the first tool for the automatic detection of runtime errors at compilation time through static analysis of C and Ada 83 applications. The tool relies on Abstract Interpretation techniques to detect the following categories of errors :

• Out of Bounds Array Index,
• Illegal Dereference of Pointer,
• Uninitialized Pointer,
• Uninitialized Variable,
• Uninitialized Value Returned (by function),
• User Assertion Failure,
• Power Must Be Positive,
• Division by Zero,
• Shift Amount Within Bounds,
• Overflow,
• Underflow,
• Arithmetic Exceptions,
• Non Termination of Call,
• Non Termination of Loop,
• Unreachable Code,
• Uncalled Procedure,
• Concurrent Access to Shared Variables.
  

The main benefit of Polyspace Verifier is its ease of use :

• No test case to write
  Find the bugs that you generally find but much faster
• No execution but exhaustive analysis
  Find the bugs that you generally don't find because of
  missing test cases
  

• No instrumentation
  Find the bugs that you generally don't find in absence of code instrumentation on target (memory corruption)
  
• No change to development process
  Source code only is required

The final result is a complete and precise location of errors in the source code.