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:
Combining abstract interpretation and static code analysis enables you to:
For details, see Polyspace® products.
Examples and How To
See also: 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