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 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:

For details, see Polyspace® products.

See also: Polyspace Bug Finder, Polyspace Code Prover, Static analysis with Polyspace products, verification, validation, and test, embedded systems, abstract interpretation, code review, cyclomatic complexity, formal methods, software metrics, software QA, software quality objectives, source code analysis, static code analysis