Abstract Interpretation

Detecting and proving the absence of run-time errors

Abstract interpretation is a formal methods technique that relies on a broad base of mathematical theorems that define rules for analyzing complex dynamic systems such as software applications. Instead of analyzing each state of a program, abstract interpretation represents these states in a more general form and provides rules to manipulate them. It produces a mathematical abstraction and also interprets the abstraction.

To produce a mathematical abstraction of program states, abstract interpretation thoroughly analyzes all code variables. When combined with non-exponential algorithms and today's increased processing power, it helps to address complex embedded software verification and testing challenges.

You can use abstract interpretation with static code analysis to perform code verification to identify and diagnose run-time errors such as overflows, divide by zeros, and out of bound pointers. Metrics produced by this process provide a means to measure and improve software quality. When applied to the detection of run-time errors, abstract interpretation completely and comprehensively verifies all risky operations and automatically provides a diagnostic of "proven," "fail," "unreachable," or "unproven" for each operation.

Combining abstract interpretation and static code analysis lets you:

• Detect elusive run-time errors
• Prove the absence of certain run-time errors

Polyspace products are static analysis tools that use abstract interpretation. They perform static analysis to detect run-time errors and prove the absence of certain run-time errors in C/C++ and Ada source code. They also produce code quality metrics and check source code for compliance to code standards such as MISRA-C/C++ and JSF++.

Examples and How To

• Code Verification and Run-Time Error Detection Through Abstract Interpretation (White Paper)
• Proving the Absence of Run-Time Errors 3:44 (Video)

Software Reference

• Polyspace Client for C/C++ (Product)
• Polyspace Client for Ada (Product)

See also: Polyspace code verification products, verification, validation, and test, embedded systems