What Is Abstract Interpretation?

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 accomplish the following tasks:

• Perform code verification to identify and diagnose run-time errors
• Use metrics produced by this process to measure and improve software quality
• Verify completely and comprehensively all risky operations, getting a diagnostic of “proven,” “fail,” “unreachable,” or “unproven” for each operation

Combining abstract interpretation and static code analysis enables you to:

• Detect elusive run-time errors
• Prove the absence of certain run-time errors
• Produce code quality metrics
• Check source code for compliance to code standards such as MISRA C and JSF++

For details, see Polyspace^® products.