Widening (computer science)

Last updated August 24, 2019

In computer science, especially model checking and abstract interpretation, widening refers to at least two different techniques in the analysis of abstract transition systems where infinite progressions of abstract states are replaced by a (computed or guessed^[1]) least fixed point. The use of the term in model checking is closely related to acceleration techniques, some authors reserving acceleration for exact computations.^[2]

Computer science is the study of processes that interact with data and that can be represented as data in the form of programs. It enables the use of algorithms to manipulate, store, and communicate digital information. A computer scientist studies the theory of computation and the practice of designing software systems.

In computer science, model checking, or property checking, is, for a given finite-state model of a system, exhaustively and automatically checking whether this model meets a given specification. Typically, one has hardware or software systems in mind, whereas the specification contains safety requirements such as the absence of deadlocks and similar critical states that can cause the system to crash, as well as liveness requirements.

In computer science, abstract interpretation is a theory of sound approximation of the semantics of computer programs, based on monotonic functions over ordered sets, especially lattices. It can be viewed as a partial execution of a computer program which gains information about its semantics without performing all the calculations.

Intuition

While many computer programs can be understood in terms of machine states and transitions (see formal semantics of programming languages), their state spaces may be too large to fully represent and analyse. Modern analysis techniques therefore try to reason about abstract states, which correspond to many concrete states.

Abstraction Model checking is for systems where an actual representation is too complex in developing the model alone. So, the design undergoes a kind of translation to scaled down "abstract" version.

Often, the abstract states are structured in such a way that by repeatedly following the effect of program steps or by coarsening the abstraction, one obtains a chain of abstractions that is proven to terminate.

Use in Model Checking

Widening techniques and the closely related acceleration techniques are used in the forward analysis of systems in the discipline of symbolic model checking. The techniques detect cycles, i.e. sequences of abstract state transitions that could be repeated. When such a sequence can be repeated over and over, yielding new states (e.g. a variable might be incremented at every repetition), the symbolic analysis of the program will not explore all of these states in finite time. For several important families of systems such as pushdown systems, channel systems or counter systems, subclasses amenable to so-called flat acceleration have been identified^[2] for which a complete analysis procedure exists that computes the whole set of reachable states. This type of forward analysis is also related to well structured transition systems, but well-structuredness alone is not sufficient for such procedures to be complete (for example, the coverability graph of a Petri net is always finite but in general, it overapproximates the true state space).

In computer science, specifically in the field of formal verification, well-structured transition systems (WSTSs) are a general class of infinite state systems for which many verification problems are decidable, owing to the existence of a kind of order between the states of the system which is compatible with the transitions of the system. WSTS decidability results can be applied to Petri nets, lossy channel systems, and more.

A Petri net, also known as a place/transition (PT) net, is one of several mathematical modeling languages for the description of distributed systems. It is a class of discrete event dynamic system. A Petri net is a directed bipartite graph, in which the nodes represent transitions and places. The directed arcs describe which places are pre- and/or postconditions for which transitions. Some sources state that Petri nets were invented in August 1939 by Carl Adam Petri—at the age of 13—for the purpose of describing chemical processes.

Use in Abstract Interpretation

Cousot and Cousot ^[3] have introduced a notion of widening while defining the framework of abstract interpretation. An example for the widening of an abstract domain that appears in abstract interpretation^[4]^[5] would be replacing the upper bound of an interval by $\infty$ .

Related Research Articles

A finite-state machine (FSM) or finite-state automaton, finite automaton, or simply a state machine, is a mathematical model of computation. It is an abstract machine that can be in exactly one of a finite number of states at any given time. The FSM can change from one state to another in response to some external inputs; the change from one state to another is called a transition. An FSM is defined by a list of its states, its initial state, and the conditions for each transition. Finite state machines are of two types – deterministic finite state machines and non-deterministic finite state machines. A deterministic finite-state machine can be constructed equivalent to any non-deterministic one.

Static program analysis is the analysis of computer software that is performed without actually executing programs, in contrast with dynamic analysis, which is analysis performed on programs while they are executing. In most cases the analysis is performed on some version of the source code, and in the other cases, some form of the object code.

A Turing machine is a mathematical model of computation that defines an abstract machine, which manipulates symbols on a strip of tape according to a table of rules. Despite the model's simplicity, given any computer algorithm, a Turing machine capable of simulating that algorithm's logic can be constructed.

In software engineering and computer science, abstraction is:

An abstract machine, also called an abstract computer, is a theoretical model of a computer hardware or software system used in automata theory. Abstraction of computing processes is used in both the computer science and computer engineering disciplines and usually assumes a discrete time paradigm.

In computer science, specifically software engineering and hardware engineering, formal methods are a particular kind of mathematically based techniques for the specification, development and verification of software and hardware systems. The use of formal methods for software and hardware design is motivated by the expectation that, as in other engineering disciplines, performing appropriate mathematical analysis can contribute to the reliability and robustness of a design.

In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics.

A formal system is used to infer theorems from axioms according to a set of rules. These rules used to carry out the inference of theorems from axioms are known as the logical calculus of the formal system. A formal system is essentially an "axiomatic system". In 1921, David Hilbert proposed to use such system as the foundation for the knowledge in mathematics. A formal system may represent a well-defined system of abstract thought.

Computability is the ability to solve a problem in an effective manner. It is a key topic of the field of computability theory within mathematical logic and the theory of computation within computer science. The computability of a problem is closely linked to the existence of an algorithm to solve the problem.

Computable functions are the basic objects of study in computability theory. Computable functions are the formalized analogue of the intuitive notion of algorithm, in the sense that a function is computable if there exists an algorithm that can do the job of the function, i.e. given an input of the function domain it can return the corresponding output. Computable functions are used to discuss computability without referring to any concrete model of computation such as Turing machines or register machines. Any definition, however, must make reference to some specific model of computation but all valid definitions yield the same class of functions. Particular models of computability that give rise to the set of computable functions are the Turing-computable functions and the μ-recursive functions.

Model-based testing is an application of model-based design for designing and optionally also executing artifacts to perform software testing or system testing. Models can be used to represent the desired behavior of a system under test (SUT), or to represent testing strategies and a test environment. The picture on the right depicts the former approach.

Computational mechanics is the discipline concerned with the use of computational methods to study phenomena governed by the principles of mechanics. Before the emergence of computational science as a "third way" besides theoretical and experimental sciences, computational mechanics was widely considered to be a sub-discipline of applied mechanics. It is now considered to be a sub-discipline within computational science.

In probability theory, a Markov model is a stochastic model used to model randomly changing systems. It is assumed that future states depend only on the current state, not on the events that occurred before it. Generally, this assumption enables reasoning and computation with the model that would otherwise be intractable. For this reason, in the fields of predictive modelling and probabilistic forecasting, it is desirable for a given model to exhibit the Markov property.

CADP is a toolbox for the design of communication protocols and distributed systems. CADP is developed by the CONVECS team at INRIA Rhone-Alpes and connected to various complementary tools. CADP is maintained, regularly improved, and used in many industrial projects.

Device driver synthesis and verification

Device drivers are programs which allow software or higher-level computer programs to interact with a hardware device. These software components act as a link between the devices and the operating systems, communicating with each of these systems and executing commands. They provide an abstraction layer for the software above and also mediate the communication between the operating system kernel and the devices below.

Astrée is a static analyzer based on abstract interpretation. It analyzes programs written in the C programming language and outputs an exhaustive list of possible runtime errors and assertion violations. The defect classes covered include divisions by zero, buffer overflows, dereferences of null or dangling pointers, data races, deadlocks, etc. Astrée includes a static taint checker and helps finding cybersecurity vulnerabilities, such as Spectre.

AbsInt is a software-development tools vendor based in Saarbrücken, Germany. The company was founded in 1998 as a technology spin-off from the Department of Programming Languages and Compiler Construction of Prof. Reinhard Wilhelm at Saarland University. AbsInt specializes in software-verification tools based on abstract interpretation. Its tools are used worldwide by Fortune 500 companies, educational institutions, government agencies and startups.

Radhia Cousot Inventor of abstract interpretation

Radhia Cousot was a French computer scientist known for inventing abstract interpretation.

References

↑ Ahmed Bouajjani and Tayssir Touili (2012), "Widening techniques for regular tree model checking", STTT, Vol. 14, No. 2, pp. 145 -- 165
1 2 Sébastien Bardin, Alain Finkel, Jérôme Leroux and Philippe Schnoebelen, Flat acceleration in symbolic model checking (2005), Automated Technology for Verification and Analysis, pp. 474--488, Springer
↑ Patrick Cousot and Radhia Cousot, Abstract Interpretation: {A} Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints (1977), Conference Record of the Fourth {ACM} Symposium on Principles of Programming Languages, Los Angeles, California, USA, January 1977, pp. 238 -- 252
↑ P. Cousot, R. Cousot (Aug 1992). "Comparing the Galois Connection and Widening / Narrowing Approaches to Abstract Interpretation" (PDF). In Maurice Bruynooghe and Martin Wirsing (ed.). Proc. 4th Int. Symp. on Programming Language Implementation and Logic Programming (PLILP). LNCS. 631. Springer. pp. 269–296.
↑ Agostino Cortesi (Aug 2008), Widening Operators for Abstract Interpretation (PDF)

This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.

[BT12-1] Ahmed Bouajjani and Tayssir Touili (2012), "Widening techniques for regular tree model checking", STTT, Vol. 14, No. 2, pp. 145 -- 165

[BardinEtAl-2] 1 2 Sébastien Bardin, Alain Finkel, Jérôme Leroux and Philippe Schnoebelen, Flat acceleration in symbolic model checking (2005), Automated Technology for Verification and Analysis, pp. 474--488, Springer

[CC77-3] Patrick Cousot and Radhia Cousot, Abstract Interpretation: {A} Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints (1977), Conference Record of the Fourth {ACM} Symposium on Principles of Programming Languages, Los Angeles, California, USA, January 1977, pp. 238 -- 252

[4] P. Cousot, R. Cousot (Aug 1992). "Comparing the Galois Connection and Widening / Narrowing Approaches to Abstract Interpretation" (PDF). In Maurice Bruynooghe and Martin Wirsing (ed.). Proc. 4th Int. Symp. on Programming Language Implementation and Logic Programming (PLILP). LNCS. 631. Springer. pp. 269–296.

[5] Agostino Cortesi (Aug 2008), Widening Operators for Abstract Interpretation (PDF)