QPR Product Banner

OUR PRODUCT – QPR REFINE

QPR-Refine offers the ideal solution for developers and software testers that are not satisfied with the results of their static code analysis tool. Our innovative verification approach is based on an exact static code analysis with highest precision. In comparison to other available tools it features precise automatic analysis reports as well as exact error traces in addition to the following benefits:

Software Quality

IMPROVE SOFTWARE QUALITY
Fewer software errors through innovative, verifiying static code analysis.

Time-to-market

REDUCE TIME-TO-MARKET
Reduce test- and development- cycles and secure short lead times.

residual risk

REDUCE RESIDUAL RISK
Avoid justification and prevent dangerous misjudgments.

definite assesment

PRECISE ASSESSMENT
Fewer false-positives by marking source locations as secure or insecure.

rapid bug fixing

RAPID BUG
FIXING

Fully automatic and bit-precise software analysis with concrete error traces.

code comprehension

IMPROVE CODE COMPREHENSION
Innovative methods of error tracing and software visualization.

This approach checks software – without executing it – by translating it into a mathematical logic formalism, and then analyzing it fully automatically and with highest precision.

Software behavior can thus be captured for all potentially occurring situations. By using innovative program visualizations the cause of a software error becomes easily comprehensible and can be eliminated in no time.

Our innovative verification approach is based on an exact static code analysis with highest precision.  By using innovative program visualizations the cause of a software error becomes easily comprehensible and can be eliminated quickly.

QPR-Refine is built in layers, for the user though only the upper layer is visible. First QPR-Refine translates the C(++)-Code gradually and with highest-precision into a mathematical logic formalism without executing it. Newest logic solver technology is then analyzing it fully automatically and with highest
precision. After that the logic proof will be re-translated step-by-step into the source code layer, resulting in concrete and bit-precise error traces for each error.

The following fault classes  can be checked fully automatically and decidably:

  • Arithmetic faults
    • Over-/under-flow
    • Division by zero
  • Bit operator faults (invalid bit shift)
  • Memory faults
    • Array index out of bound
    • Buffer overflow
    • Illegal pointer access
    • Pointer dereference
    • Memory leaks
    • Invalid/double free
    • Use after free
  • User defined properties (Assertions)