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.

  In the three years following its creation, PolySpace has confirmed its position as leader in static verification for embedded applications. Based on a highly innovative mathematical approach, PolySpace Verifier is the first software product capable of performing an exhaustive, automatic verification of a program's source code and detecting runtime errors at compilation time. In 2001, PolySpace totalled an income of over 2.4 million euros having worked with some high-ranking companies in the avionics, aerospace, defence, railways, automotive, energy and telecom fields.
For further information: