Abstract Interpretation Idea

Description

This lecture introduces the concept of abstract interpretation as a method to infer properties of program computations. It covers the basic idea, abstract states, fixpoints, control-flow graphs, and sets of states at program points. The lecture also discusses proving through fixpoints of approximate functions, reachable states as recursive equations, and analysis domains. It explains the approximation of sets, transfer functions, and updating sets in the context of program meaning and recursive equations.

Official source

https://mediaspace.epfl.ch/media/0_5ijgftx3

About this result

This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.

Data-flow analysis

Data-flow analysis is a technique for gathering information about the possible set of values calculated at various points in a computer program. A program's control-flow graph (CFG) is used to determine those parts of a program to which a particular value assigned to a variable might propagate. The information gathered is often used by compilers when optimizing a program. A canonical example of a data-flow analysis is reaching definitions.

Primitive recursive function

In computability theory, a primitive recursive function is, roughly speaking, a function that can be computed by a computer program whose loops are all "for" loops (that is, an upper bound of the number of iterations of every loop can be determined before entering the loop). Primitive recursive functions form a strict subset of those general recursive functions that are also total functions. The importance of primitive recursive functions lies in the fact that most computable functions that are studied in number theory (and more generally in mathematics) are primitive recursive.

Control-flow graph

In computer science, a control-flow graph (CFG) is a representation, using graph notation, of all paths that might be traversed through a program during its execution. The control-flow graph was discovered by Frances E. Allen, who noted that Reese T. Prosser used boolean connectivity matrices for flow analysis before. The CFG is essential to many compiler optimizations and static-analysis tools. In a control-flow graph each node in the graph represents a basic block, i.e.

State (computer science)

In information technology and computer science, a system is described as stateful if it is designed to remember preceding events or user interactions; the remembered information is called the state of the system. The set of states a system can occupy is known as its state space. In a discrete system, the state space is countable and often finite. The system's internal behaviour or interaction with its environment consists of separately occurring individual actions or events, such as accepting input or producing output, that may or may not cause the system to change its state.

Control flow

In computer science, control flow (or flow of control) is the order in which individual statements, instructions or function calls of an imperative program are executed or evaluated. The emphasis on explicit control flow distinguishes an imperative programming language from a declarative programming language. Within an imperative programming language, a control flow statement is a statement that results in a choice being made as to which of two or more paths to follow.