China 
Africa 
Explore chapters and articles related to this topic
Formal Property Verification
Published in Luciano Lavagno, Igor L. Markov, Grant Martin, Louis K. Scheffer, Electronic Design Automation for IC System Design, Verification, and Testing, 2017
Limor Fix, Ken McMillan, Norris Ip, Leopold Haller
In fact, the key to all known methods for verifying large, complex systems is abstraction. Abstraction may involve replacing a complex system with a simpler system that captures the required properties or focusing on certain relevant aspects of the system under analysis and ignoring others. An abstract system can be constructed manually, in which case we must prove that the abstract system in fact preserves the properties of interest. Alternatively, an abstraction can be constructed automatically, perhaps according to parameters given by the user. A general framework for this approach is provided by abstract interpretation [66], which was developed in the context of software verification. In this framework, the user chooses a suitable representation for facts about data in the system, and an automatic analysis computes the strongest inductive invariant of the system that can be expressed in this representation. As an example, we might use a representation that can express all linear affine relations between program variables. An important instance of abstract interpretation is predicate abstraction [67]. Here, the user provides a set of simple predicates, like x < y. The analysis constructs the strongest inductive invariant that can be expressed as a Boolean combination of these predicates.
A
Published in Phillip A. Laplante, Dictionary of Computer Science, Engineering, and Technology, 2017
abstract interpretation a partial execution of a program which gains information about its semantics (e.g., control structure, flow of information) without performing all the calculations. Abstract interpretation is typically used by compilers to analyze programs in order to decide whether certain optimizations or transformations are applicable. The objects manipulated by the program (typically values and functions) are represented by points in some domain. Each abstract domain point represents some set of real values.
Mixed-language automatic differentiation
Published in Optimization Methods and Software, 2018
Valérie Pascual, Laurent Hascoët
Static data-flow analysis [10] is an essential step to achieve efficient differentiation with a source-to-source AD tool. The goal of static data-flow analysis is to provide information on the data computed and returned by a program without knowing the values of the program's run-time inputs. In other words, static data-flow analysis extracts useful information on the program at compile time, this information being thus valid for any run-time execution on any inputs. Obviously, such an information can only be partial and must often resort to the undecidable ‘I don't know’ reply in addition to ‘yes’ or ‘no’. Abstract interpretation [4] is a framework for static data-flow analysis in which the values computed in the original code are replaced with abstract values containing the propagated abstract information. One classical example of the abstract information that one may want to propagate is the interval in which the run-time value will range, or the set of possible destinations of each pointer variable. Starting from some abstract information on the inputs or outputs (which may be empty), abstract interpretation propagates it through the program, possibly guided by its control-flow structure. Instead of a true execution of the program, possible only at run-time, this propagation must stand for every possible execution path. Some data-flow analyses follow these paths forward, others need to follow them backward. As call graphs may be cyclic in general (recursivity), and flow graphs may be cyclic (loops), completion of the analysis requires the reaching of a fixed point both on the call graph and on each flow graph. The abstract domain in which the propagated information range is designed in such a way that this fixed point is reached in a finite number of iterations. Most of the classical data-flow analyses prove useful for AD as well as specific analyses such as activity and TBR analyses [8,14]. In most AD-specific data-flow analysis, the abstract information is, for each variable v, a boolean value (e.g. does v influence the output in a differentiable way?) or a set of other variables (e.g. which input variables have a differentiable influence on v?).