Abstract: We propose a simple order-theoretic generalization of set-theoretic inductive definitions. This generalization covers inductive, co-inductive and bi-inductive definitions and is preserved by abstraction. This allows the structural operational semantics to describe simultaneously the finite/terminating and infinite/diverging behaviors of programs. This is illustrated on the structural bifinitary small/big-step trace/relational/operational semantics of the call-by-value lambdal-calculus.

Abstract: Earley's parsing algorithm is shown to be an abstract interpretation of a refinement of the derivation semantics of context-free grammars

Abstract: We discuss the scope of program analysis and enumerates the main approaches to it. The main focus is on approximate methods and, in particular, abstract interpretation. Its aspects and open problems are examined both from a theoretical and a practical point of view

Abstract: In abstract model-checking, the semantics of an infinite transition system is abstracted to get a finite approximation on which temporal-logic/mu-calculus model-checking can be directly applied. The paper proposes two improvements of abstract model-checking which can be applied to infinite abstract transition systems: <UL> <LI>A new combination of forwards and backwards abstract fixed-point model-checking computations for universal safety. It computes a more precise result than that computed by conjunction of the forward and backward analyses alone, without needing to refine the abstraction; <LI>When abstraction is unsound (as can happen in minimum/maximum path-length problems), it is proposed to use the partial results of a classical combination of forward and backward abstract interpretation analyzes for universal safety in order to reduce, on-the-fly, the concrete state space to be searched by model-checking. </UL>

Abstract: Program analysis should evolve from a disparate collection of methods and algorithms to a mature discipline founded on a well-established methodology. Abstract interpretation can be used as a basis for such a methodology.

Abstract: A short survey of abstract interpretation

Abstract: <P>We formalize Burstall's (1974) intermittent assertions method (initially conceived for proving total correctness of sequential programs) and generalize it to handle inevitability proofs for nondeterministic transition systems, hence (in particular) parallel programs. </P><P> Programs are modeled by transition systems, program executions by sets of complete traces and program properties by inevitability properties of transition systems (generalizing total correctness of programs). It follows that the study is independent of any particular programming language. </P><P> The basic proof principle that we derive from Burstall's and Manna and Waldinger's (1978) description of the intermittent assertions method is shown to be sound. It is also semantically complete under a condition on execution traces and inevitable properties. This condition is satisfied when considering inevitability properties such as total correctness or properties involving unary assertions on states. However, we conjecture that (even for deterministic programs) the basic proof principle is not complete when considering arbitrary binary inevitability properties (which relate state values at different �time instants�). </P><P> This conjecture leads us to a generalization of Burstall's intermittent assertions method using transfinite induction (to handle unbounded nondeterminism) and using auxiliary or ghost variables in the limited form of ternary intermittent assertions (which can relate state values on program entry and at two other different �time instants�). </P><P> From this generalized proof principle we derive a series of induction principles so as to broaden the allowable forms of proofs. Also we obtain more abstract and hence better understood formalizations of Burstall's method. </P><P> All proof principles are sound and semantically complete (essentially, as noticed by Manna and Waldinger, because Burstall's method can be used to express �à la Floyd� proofs). However, we prove a stronger semantic completeness result in the sense that the propositions and lemmas involved in �à la Burstall� inevitability proofs can be chosen freely (at least under necessary and sufficient conditions that we specify accurately).

Abstract: We introduce abstract interpretation frameworks which are variations on the archetypal framework using Galois connections between concrete and abstract semantics, widenings and narrowings and are obtained by relaxation of the origin al hypotheses. We consider various ways of establishing the correctness of an abstract interpretation depending on how the relation between the concrete and abstract semantics is defined. We insist upon those correspondences allowing for the inducing of the approximate abstract semantics from the concrete one. Furthermore we study various notions of widening and narrowing as a means of obtaining convergence in the iterations used in abstract interpretation.

Abstract: Abstract interpretation is a theory of semantics approximation which is used for the construction of semantics-based program analysis algorithms (sometimes called ``data flow analysis''), the comparison of formal semantics (e.g. construction of a denotational semantics from an operational one), the design of proof methods, etc. Automatic program analyzers are used for determining statically conservative approximations of dynamic properties of programs. Such properties of the run-time behavior of programs are useful for debugging (e.g. type inference), code optimization (e.g. compile-time garbage collection, useless occur-check elimination), program transformation (e.g. partial evaluation, parallelization) and even program correctness proofs (e.g. termination proof). After a few simple introductory examples we recall the classical framework for abstract interpretation of programs. Starting from a standard operational semantics formalized as a transition system, classes of program properties are first encapsulated in collecting semantics expressed as fixpoints on partial orders representing concrete program properties. We consider invariance properties characterizing the descendant states of the initial states (corresponding to top/down or forward analyzes), ascendant states of the final states (corresponding to bottom/up or backward analyzes) as well as a combination of the two. Then we choose specific approximate abstract properties to be gathered about program behaviors and express them as elements of a poset of abstract properties. The correspondence between concrete and abstract properties is established by a concretization and abstraction function which is a Galois connection formalizing the loss of information. We can then constructively derive the abstract program properties from the collecting semantics by a formal computation leading to a fixed point expression in terms of abstract operators on the domain of abstract properties. The design of the abstract interpreter then involves the choice of a chaotic iteration strategy to solve this abstract fixed point equation. We insist on the compositional design of this abstract interpreter which is formalized by a series of propositions for designing Galois connections (such as Moore families, decomposition by partitioning, reduced product, down-set completion, etc.). Then we recall the convergence acceleration methods using widening and narrowing allowing for the use of very expressive infinite domains of abstract properties. We show that this classical formal framework can be applied in extenso to logic programs. For simplicity we use a variant of SLD-resolution as the standard operational semantics. The first example is groundness analysis which is a variant of Mellish mode analysis. It is extended to a combination of top/down and bottom/up analyzes. The second example is the derivation of constraints among argument sizes which involves an infinite abstract domain requiring the use of convergence acceleration methods. We end up with a short thematic guide to the literature on abstract interpretation of logic programs.

Abstract: Generalized Hoare logic (GHL) is a formal logical system for proving invariance properties of programs. It was first introduced by Lamport to reason about simple concurrent programs with shared variables. It was generalized by Lamport and Schneider who noticed that the inference rules for each language construct (enabling invariance properties of statements to be derived from invariance properties of their components) can be viewed as special cases of simple logical meta-rules. We give a rigorous definition of GHL, based upon an abstract formalization of the syntax and semantics of programs so as to provide an interpretation for formulas of GHL which is independent of the specific instructions of the programming language used. We prove that the proof system of GHL is sound and relatively complete under hypotheses, which we formulate independently of any programming language; these are simple conditions which relate the axiom schemata for atomic actions and the axiom schemata, which define the control flow semantics, to the semantics of programs.

Abstract: We propose and compare two induction principles called &#8220;always&#8221; and &#8220;sometime&#8221; for proving inevitability properties of programs. They are respective formalizations and generalizations of Floyd invariant assertions and Burstall intermittent assertions methods for proving total correctness of sequential programs whose methodological advantages or disadvantages have been discussed in a number of previous papers. Both principles are formalized in the abstract setting of arbitrary nondeterministic transition systems and illustrated by appropriate examples. The &#8220;sometime&#8221; method is interpreted as a recursive application of the &#8220;always&#8221; method. Hence &#8220;always&#8221; can be considered as a particular case of &#8220;sometime&#8221;. These proof methods are strongly equivalent in the sense that a proof by one induction principle can be rewritten into a proof by the other one. The first two theorems of the paper show that an invariant for the &#8220;always&#8221; method can be translated into an invariant for the &#8220;sometime&#8221; method even if every recursive application of the later is required to be of finite length. The third and main theorem of the paper shows how to translate an invariant for the &#8220;sometime&#8221; method into an invariant for the &#8220;always&#8221; method. It is emphasized that this translation technique follows the idea of transforming recursive programs into iterative ones. Of course a general translation technique does not imply that the original &#8220;sometime&#8221; invariant and the resulting &#8220;always&#8221; invariant are equally understandable. This is illustrated by an example.

Abstract: Let F be a monotone operator on the complete lattice L into itself. Tarski's lattice theoretical fixed point theorem states that the set of fixed points of F is a nonempty complete lattice for the ordering of L. We give a constructive proof of this theorem showing that the set of fixed points of F is the image of L by a lower and an upper preclosure operator. The preclosure operators are the composition of lower and upper closure operators which are defined by means of limits of stationary transfinite iteration sequences for F. In the same way we give a constructive characterization of the set of common fixed points of a family of commuting operators. Finally we examine some consequences of additional semi-continuity hypotheses.

Abstract: The classical programming languages such as Pascal or ALGOL 68 do not provide full data type security. Run-time errors are not precluded on basic operations. Type safety necessitates a refinement of the data type notion which allows subtypes. The compiler must also be able to ensure that basic operations are applicable. This verification consists in determining a local subtype of globally declared variables or constants. This may be achieved by improved compiler capabilities to analyze the program properties or by kanguage constructs which permit the expression of these properties. Both approaches are discussed and illustrated by the problem of access to records via pointers, access to variants of record structures, determination of disjoint collections of linked records, and determination of integer subrange. Both approaches are complementar and a balance must be found between what must be specified by the programmer and what must be discovered by the compiler.

Abstract: The problem of discovering invariant assertions of programs is explored in light of the fixed point approach in the static analysis of programs. In section 2 we establish the lattice theoretic foundations upon which the synthesis of invariant assertions is based. We study the resolution of a fixpoint system of equations by Jacobi's successive approximation method. Under continuity hypothesis we show that any chaotic iterative method converges to the optimal solution. In section 3 we study the deductive semantics of programs. We show that a system of logical forward equations can be associated with a program using the predicate transformer rules which define the semantics of elementary instructions. The resolution of this system of semantic equations by chaotic iterations leads to the optimal invariants which exactly define the semantics of this program. Therefore the optimal invariants can be used for total correctness proffs (section 4). Next we show that usually a system of inequations is used as a substitute for the system of equations. Hence the solutions to this system of inequations are approximate invarians which can only be used for proofs of partial correctness (section 5). In section 6 we show that symbolic execution of programs concists in fact in solving the semantic equations associated with this program. The construction of the symbolic execution tree corresponds to the chaotic successive approximations method. Therefore symbolic execution permits optimal invariants to be discovered provided that one can pass to the limit, that is consider infinite paths in the symbolic execution tree. Induction principles can be used for that purpose. In section 7 we show that an approximation of the optimal solution to a fixed point system of equations can be obtained by strenghthening the term of a chaotic iteration sequence. This formalizes the synthesis of approximate invariants by heuristic methods. Various examples provide a helpful intuitive support to the technical sections.

Abstract: A brief introduction to the theory of Abstract Interpretation, examplified by constructing a hierarchy of partial traces, reflexive transitive closure, reachable states and intervals abstract semantics of transition systems.

Abstract: We present in extenso the calculation-based development of a generic compositional reachability static analyzer for a simple imperative programming language by abstract interpretation of its formal rule-based/structured small-step operational semantics.

Abstract: Formalizing ideas of FLOYD [1967a] and NAUR [1966] which, in essence, were already present in GOLDSTINE & VON NEUMANN [1947] and TURING [1949] (as recalled in MORRIS & JONES [1984]), C. A. R. Hoare introduced in October 1969 an axiomatic method for proving that a program is partially correct with respect to a specification (HOARE [1969], see the genesis and reprint of this paper in HOARE & JONES [1989, pp. 45-58]). This paper introduced or revealed a number of ideas which originated an evolution of programming from arts and crafts to a science. Hoare logic had a very significant impact on program verification and design methods. It was an essential step in the emergence of �structured programming� in the 1970's. It is also an important contribution to the development of formal semantics of programming languages. Understanding that programs can be a subject of mathematical investigations was also crucial in the development of a theory of programming. This is reflected in the fact that HOARE [1969] is one of the most widely cited papers in computing science (see the bibliography of more than 350 references).

Abstract: Abstracting from Floyd's invariant assertions and well-ordered set method for proving total correctness of sequential programs, we present induction principles for proving inevitability properties of transition systems. These induction principles are shown to be sound, semantically complete and equivalent. This formalizes Floyd's method independently of any particular programming and assertion language and generalizes it to non-deterministic transition systems (in particular partitionned ones) hence to parallel programs. Considering various classes of bounded nondeterminacy, we characterize the corresponding well-founded relations which are necessary and sufficient for compelteness. <BR> &nbsp;&nbsp;&nbsp;When the behavior of the transition system is specified by a non-closed set of execution traces (e.g. fair parallelism), Floyd's computational induction method cannot be applied without auxiliary variables. One approach consists in using Floyd's method for an auxiliary transition relation on states and history variables that exactly generates the original set of traces. Another approach consists in a generalization of the use of loop cutpoints in Floyd's method, in that the choice of the cutpoints (where some termination function has to be decreased) may depend upon computation histories cumulated into auxiliary variables.

Abstract: A program defines a dynamic discrete system that is a transition relation on states. In section 4, we set-up general mathematical methods useful in the task of analyzing the behavior of dynamic discrete systems. In order to make this mathematically demanding sections self-contained, lattice-theoretical theorems on fixed points of isotone or continuous maps are first introduced in a separate subsection. The main result of section 4 shows that the predicates characterizing the descendants of the entry states, the ascendants of the exit states, the states which lead to an error, and the states which cause the system to diverge are the least or greatest solution to forward or backward fixed point equations. This result is completed by the proof that whenever a forward equation (corresponding to postconditions) is needed, a backward equation (corresponding to preconditions) can be used instead, and vice-versa. Finally we show that when a set of states of the dynamic discrete system is partitioned, the forward and backward equation can be decomposed into a system of equations. Numerous examples of applications are given which provide for a very concise presentation and justification of classical or innovative program proving methods. Section 5 tailors the general mathematical techniques previously set up for analyzing the behavior of a deterministic discrete dynamic system to suit the particular case when the system is a program. Two main theorems make explicit the syntactic construction rules for obtaining the systems of semantic backward or forward equations from the text of a program. The facts that the extreme fixed points of these systems of semantic equations can lead to complete information about program behavior and that the backward and forward approaches are equivalent are illustrated on the simple introductory example. In the second part we briefly survey our joint work with Radhia Cousot on the automatic synthesis of approximate invariant assertions for programs. Because of well-known insolvability problems, the semantics equations which have been used in section 5 for program analysis cannot be algorithmically solved. hence we must limit ourselves to constructive methods which automatically compute approximate solutions? Such approximate information about the program behavior is often useful, e.g., in program verification systems, program debugging systems, optimizing compilers, etc. Approximate solutions to the semantic equations can be obtained by first simplifying these equations and next solving the simplified equations associated with the program text, using any chaotic iteration technique. In section 6.2 we show that when the exact solution to the simplified equations is obtained only after an infinite number of iteration steps, the convergence of the iterates can be sped up using an extrapolation technique based on a widening or narrowing operator. A hierarchy of examples illustrates the approximate program analysis method.

Abstract: <P> Abstract Interpretation is a theory of approximation of mathematical structures, in particular those involved in the semantic models of computer systems. Abstract interpretation can be applied to the systematic construction of methods and effective algorithms to approximate undecidable or very complex problems in computer science. The scope of application is rather large e.g.\ from type inference, model-checking, program transformation, watermarking to context-free grammar parser generation. </P><P> In particular, abstract interpretation-based static analysis, which automatically infers dynamic properties of computer systems, has been very successful these last years to automatically verify complex properties of real-time, safety critical, embedded systems. For example, ASTR�E can analyze mechanically and verify formally the absence of runtime errors in industrial safety-critical embedded synchronous control/command codes of several hundred thousand to one million of lines C. </P><P> We summarize the main reasons for the technical success of ASTR�E, which provides directions for application of abstract interpretation to the Verification Grand Challenge. </P>

Abstract: In this paper, we present an abstract fixpoint checking algorithm with automatic refinement by backward completion in Moore closed abstract domains. We study the properties of our algorithm and prove it to be more precise than the counterexample guided abstract refinement algorithm (CEGAR). Contrary to several works in the literature, our algorithm does not require the abstract domains to be partitions of the state space. We also show that our automatic refinement technique is compatible with so-called acceleration techniques. Furthermore, the use of Boolean closed domains does not improve the precision of our algorithm. The algorithm is illustrated by proving properties of programs with nested loops.

Abstract: We discuss the characteristic properties of ASTR&Eacute;E, an automatic static analyzer for proving the absence of runtime errors in safety-critical real-time synchronous control/command C programs, and compare it with a variety of other program analysis tools.

Abstract: Software watermarking consists in the intentional embedding of indelible stegosignatures or watermarks into the subject software and extraction of the stegosignatures embedded in the stegoprograms for purposes such as intellectual property protection. We introduce the novel concept of abstract software watermarking. The basic idea is that the watermark is hidden in the program code in such a way that it can only be extracted by an abstract interpretation of the (maybe non-standard) concrete semantics of this code. This static analysis-based approach allows the watermark to be recovered even if only a small part of the program code is present and does not even need that code to be executed. We illustrate the technique by a simple abstract watermarking protocol for methods of Java classes. The concept applies equally well to any other kind of software (including hardware originally specified by software).

Abstract: We show that abstract interpretation-based static program analysis can be made efficient and precise enough to formally verify a class of properties for a family of large programs with few or no false alarms. This is achieved by refinement of a general purpose static analyzer and later adaptation to particular programs of the family by the end-user through parametrization. This is applied to the proof of soundness of data manipulation operations at the machine level for periodic synchronous safety critical embedded software. The main novelties are the design principle of static analyzers by refinement and adaptation through parametrization, the symbolic manipulation of expressions to improve the precision of abstract transfer functions, the octagon, ellipsoid, and decision tree abstract domains, all with sound handling of rounding errors in floating point computations, widening strategies (with thresholds, delayed) and the automatic determination of the parameters (parametrized packing).

Abstract: We introduce a general uniform language-independent framework for designing online and offline source-to-source program transformations by abstract interpretation of program semantics. Iterative source-to-source program transformations are designed constructively by composition of source-to-semantics, semantics-to-transformed semantics and semantics-to-source abstractions applied to fixed point trace semantics. The correctness of the transformations is expressed through observational and performance abstractions. The framework is illustrated on three examples: constant propagation, program specialization by online and offline partial evaluation and static program monitoring.

Abstract: The purpose of this paper is to present four basic methods for compositional separate modular static analysis of programs by abstract interpretation: <UL> <LI>simplification-based separate analysis; <LI> worst-case separate analysis; <LI> separate analysis with (user-provided) interfaces; <LI>symbolic relational separate analysis; </UL> as well as a fifth category which is essentially obtained by composition of the above separate local analyzes together with global analysis methods.

Abstract: Abstract interpretation is used in program static analysis and model checking to cope with infinite state spaces and/or with computer resource limitations. One common problem is to check abstract fixed points for specifications. The abstraction is partially complete when the checking algorithm is exact in that, if the algorithm ever terminates, its answer is always affirmative for correct specifications. We characterize partially complete abstractions for various abstract fixed point checking algorithms, including new ones, and show that the computation of complete abstract domains is essentially equivalent to invariance proofs that is to concrete fixed point checking.

Abstract: We study the abstract interpretation of temporal calculi and logics in a general syntax, semantics and abstraction independent setting. This is applied to the extended reversible mu-calculus, a generalization of the mu-calculus with new reversal and abstraction modalities as well as a new time-symmetric trace-based semantics. The more classical set-based semantics is shown to be an abstract interpretation of the trace-based semantics which leads to the understanding of model-checking and its application to data-flow analysis as incomplete temporal abstract interpretations. Soundness and incompleteness of the abstractions are discussed. The sources of incompleteness, even for finite systems, are pointed out, which leads to the identification of relatively complete sublogics, à la CTL.

Abstract: # We define a hierarchy of compositional formal semantics of algebraic polynomial systems over F-algebras by abstract interpretation. This generalizes classical formal language theoretical results and context-free grammar flow-analysis algorithms in the same uniform framework of universal algebra and abstract interpretation.

Abstract: Starting from a denotational semantics of the eager untyped lambda-calculus with explicit runtime errors, the standard collecting semantics is defined as specifying the strongest program properties. By a first abstraction, a new sound type collecting semantics is derived in compositional fixpoint form. Then by successive (semi-dual) Galois connection based abstractions, type systems and/or type inference algorithms are designed as abstract semantics or abstract interpreters approximating the type collecting semantics. This leads to a hierarchy of type systems, which is part of the lattice of abstract interpretations of the untyped lambda-calculus. This hierarchy includes two new à la Church/Curry polytype systems. Abstractions of this polytype semantics lead to classical Milner/Mycroft and Damas/Milner polymorphic type schemes, Church/Curry monotypes and Hindley principal typing algorithm. This shows that types are abstract interpretations.

Abstract: <P>Grammar-based program analysis à la Jones and Muchnick and set-constraint-based program analysis à la Aiken and Heintze are static analysis techniques that have traditionally been seen as quite different from abstract-interpretation-based analyzes, in particular because of their apparent non-iterative nature. For example, on page 18 of N. Heintze thesis, it is alleged that ``The finitary nature of abstract interpretation implies that there is a fundamental limitation on the accuracy of this approach to program analysis. There are decidable kinds of analysis that cannot be computed using abstract interpretation (even with widening and narrowing). The set-based analysis considered in this thesis is one example''. </P><P> On the contrary, we show that grammar and set-constraint-based program analyzes are similar abstract interpretations with iterative fixpoint computation using either a widening or a finitary grammar/set-constraints transformer or even a finite domain for each particular program. </P><P>The understanding of grammar-based and set-constraint-based program analysis as a particular instance of abstract interpretation of a semantics has several advantages. First, the approximation process is formalized and not only explained using examples. Second, a domain of abstract properties is exhibited which is of general scope. Third, these analyses can be easily combined with other abstract-interpretation-based analyses, in particular for the analysis of numerical values. Fourth, they can be generalized to very powerful attribute-dependent and context-dependent analyses. Finally, a few misunderstandings may be removed.</P>

Abstract: We present a language and semantics-independent, compositional and inductive method for specifying formal semantics or semantic properties of programs in equivalent fixed point, equational, constraint, closure-condition, rule-based and game-theoretic form. The definitional method is obtained by extending set-theoretic definitions in the context of partial orders. It is parameterized by the language syntax, by the semantic domains and by the semantic transformers corresponding to atomic and compound program components. The definitional method is shown to be preserved by abstract interpretation in either fixpoint, equational, constraint, closure-condition, rule-based or game-theoretic form. The features common to all possible instantiations are factored out thus allowing for results of general scope such as well-definedness, semantic equivalence, soundness and relative completeness of abstract interpretations, etc. to be proved compositionally in a general language and semantics-independent framework.

Abstract: The original formulation of abstract interpretation represents program properties by sets. A property is understood as the set of semantic values satisfying it. Strongest program properties are defined by the collecting semantics which extends the standard semantics to powersets of semantic values. The approximation relation corresponding to the logical implication of program properties is subset inclusion. This was expressed using set and lattice theory in the context of transition systems that is of an operational semantics. This approach was applied to imperative programs, first-order procedures, communicating processes, parallel and logic programs. Some applications of abstract interpretation, such as strictness analysis for lazy functional languages, require infinite behaviors of higher-order functions to be taken into account. In this context denotational semantics is very natural (strictness is f(bottom)=botom where bottom denotes non-termination). The set-theoretic approach to abstract interpretation was felt incompatible with denotational semantics. The attempts to express the collecting semantics in denotational form were unsuccessful since properties of functions f in D1 --> D2 had to be expressed as continuous functions between powerdomains F in P(D1) --> P(D2) which is not expressive enough. We solve the problem by returning to the sources of abstract interpretation, which consists in considering collecting semantics such that e.g. properties of functions f in D1 --> D2 are sets of functions F in P(D1 --> D2). Various Galois connection based approximations of F in P(D1 --> D2) can then be applied. By using Galois connections, properties of the standard semantics naturally transfer to the collecting and then to the abstract semantics. This set-theoretic abstract interpretation framework is formulated in a way which is independent of both the programming language and the method used to specify its semantics. It is illustrated for a higher-order monomorphically typed lazy functional language starting from its standard denotational semantics . The chosen application is comportment analysis which generalizes strictness, termination, projection (including absence), dual projection (including totality) and PER analysis and is expressed in denotational style.

Abstract: We introduce and illustrate a specification method combining rule-based inductive definitions, well-founded induction principles, fixed-point theory and abstract interpretation for general use in computer science. Finite as well as infinite objects can be specified, at various levels of details related by abstraction. General proof principles are applicable to prove properties of the specified objects. The specification method is illustrated by introducing G^{<inline-equation><f>&infin;</f></inline-equation>}SOS, a structured operational semantics generalizing Plotkin's structural operational semantics (SOS) so as to describe the finite, as well as the infinite behaviors of programs in a uniform way and by constructively deriving inductive presentations of the other (relational, denotational, predicate transformers, ...) semantics from G^{<inline-equation><f>&infin;</f></inline-equation>}SOS by abstract interpretation.

Abstract: The use of infinite abstract domains with widening and narrowing for accelerating the convergence of abstract interpretations is shown to be more powerful than the Galois connection approach restricted to finite lattices (or lattices satisfying the chain condition).

Abstract: <P>We present semantic analysis techniques for concurrent programs which are designed as networks of nondeterministic sequential processes, communicating with each other explicitly, by the sole means of synchronous, unbuffered message passing. The techniques are introduced using a version of Hoare's programming language CSP (Communicating Sequential Processes). <P></P> One goal is to propose an invariance proof method to be used in the development and verification of correct programs. The method is suitable to partial correctness, absence of deadlocks and non-termination proofs. The design of this proof method is formalized so as to prepare the way for possible alternatives. <P></P> A complementary goal is to popose an automatic technique for gathering information about CSP programs that can be useful to both optimizing compilers and program partial verification systems. </P>

Abstract: Semantic analysis of programs is essential in optimizing compilers and program verification systems. It encompasses data flow analysis, data type determination, generation of approximate invariant assertions, etc. Several recent papers (among others Cousot & Cousot[77a], Graham & Wegman[76], Kam & Ullmann[76], Kildall[73], Rosen[75], Tarjan[76], Wegbreit[75]) have introduced abstract approaches to program analysis which are tantamount to the use of a program analysis framework (A,t,gamma) where A is a lattice of (approximate) assertions, t is an (approximate) predicate transformer and gamma is an often implicit function specifying the meaning of the elements of A. This paper is devoted to the systematic and correct design of program analysis framework with respect to a formal semantics. Preliminary definitions are given in Section 2 concerning the merge over all paths and (least) fixed point program-wide analysis methods. In Section 3 we briefly define the (forward and backward) deductive semantics of programs which is later used as a formal basis in order to prove the correctness of the approximate program analysis frameworks. Section 4 very shortly recall the main elements of the lattice theoretic approach to approximate semantic analysis of programs. The design of a space of approximate assertions A is studied in Section 5. We first justify the very reasonable assumption that A must be chosen such that the exact invariant assertions of any program must have an upper approximation in A and that the approximate analysis of any program must be performed using a deterministic process. These assumptions are shown to imply that A is a Moore family, that the approximation operator (which defines the least upper approximation of any assertion) is an upper closure operator and that A is necessarily a complete lattice. We next show that the connection between the spec of approximate assertions and a computer representation is naturally made using a pair of isotone (monotone) adjoined functions. This type of connection between complete lattices is related to Galois connections thus making available classical mathematical results. Additional results are proved, they hold when no two approximate assertions have the same meaning. In section 6 we study and exemplify various methods which can be used in order to define a space of approximate assertions or equivalently an approximation unction. They include the characterization of the least Moore family containing an arbitrary set of assertions, the construction of the least closure operator greater than or equal to an arbitrary approximation function, the definition of a space of approximate assertions by means of a complete join congruence relation of by means of a family of principal ideals. Section 7 is dedicated to the design of the approximate predicate transformer induced by a space of approximate assertions. First we look for a reasonable definition of the correctness of approximate predicate transformers and show that a local correctness condition can be given which has to be verified for every type of elementary statement. This local correctness condition ensures that the (merge over all paths or fixpoint) global analysis of any program is correct. Since isotony is not required for approximate predicate transformers to be correct, it is shown that non-isotone program analysis frameworks are manageable although it is later argued that the isotony hypothesis is natural. We next show that among all possible approximate predicate transformers which can be used with a given space of approximate assertions there exists a best one which provides the maximum information relative to a program-wide analysis method. The best approximate predicate transformer induced by a space of approximate assertions turns out to be isotone? Some interesting consequences of the existence of a best predicate transformer are examined. One is that we have in hand a formal specification of the program which have to be written in order to implement a program analysis framework once a representation of the space of approximate assertions has been chosen. Examples are given, including ones where the semantics of programs is formalized using Hoare's sets of traces. In Section 8 we show that a hierarchy of approximate analyses can be defined according to the fineness of the approximations specified by a program analysis framework. some elements of the hierarchy are shortly exhibited and related to the relevant literature. In section 9 we consider global program analysis methods. The distinction between "distributive" and "non-distributive" program analysis frameworks is studied. It is shown that when the best approximate predicate transformer is considered the coincidence or not of the merge over all paths and least fixpoint global analyses of programs is a consequence of the choice of the space of approximate assertions. It is shown that the space of approximate assertions can always be refined so that the merge over all paths analysis of a program can be defined by means of the least fixed point of isotone (monotone) equations. Section 10 is devoted to the combination of program analysis frameworks. We study and exemplify how to perform the "sum", "product" and "power" of program analysis frameworks. It is shown that combined analyzes lead to more accurate information than the conjunction of the corresponding separate analyzes but this can only be achieved by a new design of the approximate predicate transformer induced by the combined program analysis frameworks.

Abstract: The model of abstract interpretation of programs developed by Cousot & Cousot [1976] and Cousot & Cousot [1977] is applied to the static determination of linear equality or inequality relations among variables of programs.

Abstract: We present a general technique for determining properties of recursive procedures. For example, a mechanized analysis of the procedure reverse can show that whenever L is a non-empty linked linear list then reverse(L) is a non-empty linked linear list which shares no elements with L. This information about reverse approximates the fact that reverse(L) is a reversed copy of L. In section 2, we introduce U-topological lattices that is complete lattices endowed with a U-topology. The continuity of functions is characterized in this topology and fixed point theorems are recalled in this context. The semantics of recursive procedures is defined by a predicate transformer associated with the procedure. This predicate transformer is the least fixed point of a system of functional equations (§3.2) associated with the procedure by a syntactic algorithm (§3.1). In section 4, we study the mechanized discovery of approximate properties of recursive procedures. The notion of approximation of a semantic property is introduced by means of a closure operator on the U-topological lattice of predicates. Several characterizations of closure operations are given which can be used in practice to defined the approximate properties of interest (§4.1.1). The lattice of closure operators induces a hierarchy of program analyzes according to their fineness. Combinations of different analyzes are studied (§4.1.2). A closure operator defined on the semantic U-topological space induces a relative topology on the complete lattice of approximate properties, so that the space of approximate properties is a U-topological lattice (§4.1.3). Then functions and functionals on the space of semantic properties can be expressed in the space of approximate properties (§4.1.4, §4.1.5). In order to represent the space of approximate properties in a machine we use an homeomorphic space the elements of which can be represented inside a computer (§4.1.6). The systematic correspondence between semantic and approximate properties of programs, allows the association of a system of approximate functional equations with a recursive procedure (§4.1.7). Its mechanical resolution by successive approximations determines an approximate predicate transformer which is a partial representation of the meaning of the procedure (§4.2). In practice chaotic iterations are used to construct this solution when the space of approximate properties is finite (§4.2.1) but when infinite strengthened chaotic iterations must be used to accelerate the convergence (§4.2.2). Throughout the paper various practical examples are given.

Abstract: A program denotes computations in some universe of objects. Abstract interpretation of programs consists in using that denotation to describe computations in another universe of abstract objects, so that the result of abstract execution give some informations on the actual computations. An intuitive example (which we borrow from Sintzoff [72]) is the rule of signs. The text -1515*17 may be undestood to denote computations on the abstract universe {(+), (-), (+-)} where the semantics of arithmetic operators is defined by the rule of signs. The abstract execution -1515*17 ==> -(+)*(+) ==> (-)*(+) ==> (-), proves that -1515+17 is a negative number. Abstract interpretation is concerned by a particular underlying structure of the usual universe of computations (the sign, in our example). It gives a summary of some facets of the actual executions of a program. In general this summary is simple to obtain but inaccurate (e.g. -1515+17 ==> -(+)+(+) ==> (-)+(+) ==> (+-)). Despite its fundamental incomplete results abstract interpretation allows the programmer or the compiler to answer questions which do not need full knowledge of program executions or which tolerate an imprecise answer (e.g. partial correctness proofs of programs ignoring the termination problems, type checking, program optimizations which are not carried in the absence of certainty about their feasibility, ...). Section 3 describes the syntax and mathematical semantics of a simple flowchart language. This mathematical semantics is used in section 4 to built a more abstract model of the semantics of programs, in that it ignores the sequencing of control flow. This model is taken to be the most concrete of the abstract interpretations of programs. Section 5 gives the formal definition of the abstract interpretations of a program. Abstract program properties are modeled by a complete semi-lattice. Elementary program constructs are locally interpreted by order-preserving functions which are used to associate a system of equations with a program. The program global properties are then defined as one of the extreme fixed points of that system. The abstraction process is defined in section 6. It is shown that the program properties obtained by an abstract interpretation of a program are consistent with those obtained by a more refined interpretation of that program. In particular, an abstract interpretation may be shown to be consistent with the formal semantics of the language. Levels of abstraction are formalized by showing that consistent abstract interpretations form a lattice (section 7). Section 8 gives a constructive definition of abstract properties of programs based on constructive definitions of fixed points. It shows that various classical algorithms such as Kildall, Wegbreit, etc compute program properties as limits of finite Kleene sequences. Section 9 introduces finite fixed point approximation methods to be used when Kleene's sequences are infinite. They are shown to be consistent with the abstraction process. Practical examples illustrate the various sections. The conclusion points out that the abstract interpretation of programs is a unified approach to apparently unrelated program analysis techniques.

Abstract: An abstract interpreter is presented for the static analysis of imperative programs with widenings/narrowings to cope with termination when using abstract domains not satisfying the ascending chain condition. Correctness is stated with respect to a collecting semantics. Examples concern interval and pointer analysis.

Abstract: <P>In order to verify semialgebraic programs, we automatize the Floyd/Naur/Hoare proof method. The main task is to automatically infer valid invariants and rank functions. </P><P> First we express the program semantics in polynomial form. Then the unknown rank function and invariants are abstracted in parametric form. The implication in the Floyd/Naur/Hoare verification conditions is handle by abstraction into numerical constraints by Lagrangian relaxation. The remaining universal quantification is handled by semidefinite programming relaxation. Finally the parameters are computed using semidefinite programming solvers. </P><P> This new approach exploits the recent progress in the numerical resolution of linear or bilinear matrix inequalities by semidefinite programming using efficient polynomial primal/dual interior point methods generalizing those well-known in linear programming to convex optimization. </P><P> The framework is applied to total correctness of sequential, nondeterministic, concurrent, and fair parallel imperative polynomial programs and can easily be extended to other safety and liveness properties. </P>

Abstract: <B>Iterative methods for construction and approximation of fixpoints of monotone operators on lattices, program static analysis.</B> <P> Semantic program analysis consists in the determination of the conditions in which the run-time execution of a program terminates, does not terminate or leads to an error (whether because the rules of good usage of a programming language have not been respected, or because the program does not correspond to its specification). The semantic analysis of a program must also allow us to determine, in each point of the program, the properties of the objects manipulated by the program. <P> We propose a theory of the semantic analysis of programs, providing a unified framework to carry out some analyses, from the most precise ones, like the ones that are performed to justify the total correctness of programs, to the coarsest, like the ones that are used in compilation. In our opinion, there is no lack of continuity between these two extremes, and the theory we propose allows the construction of a continuous range of applications, from exact analysis to the most approximate analyses. Since we care about practical applications, we have devoted part of our efforts to build up a model leading to automatized solutions, (some automatizations having effectively been realized), to economically relevant problems. <UL> <LI> In most systems for program verification, the semantic analysis of the program to be justified must be done by the programmer, who has to provide a documentation of the program, often heavy because of the amount of details. Now, if we exclude the specific issue describing the problem to solve, a fair amount of this documentation can be offered by the text of the program (with the certainty that this documentation and the program itself are in accordance). <LI> The program debugging techniques, still widely used in computer software industry can be partly avoided (at least for the programming mistakes, if not for the design mistakes), using our ideas for an automatic semantic analysis of the programs, and this, without waiting for the ten, or more, years, necessary for the theorem prover based techniques of program verification to be made practical. On the other hand, it is for certain that the methods we propose are complementary and offer, for some kinds of analyses, a very profitable cost/benefit ratio. <LI> In high-level languages, the programmer is encouraged to formulate his/her algorithms in abstract terms, appropriate to the problem to be solved. To make an automatic choice for an effective program implementation, one has to make a rather precise semantic analysis of it. <LI> Almost all the definitions of classic programming languages contain various restrictions which are necessary for the programs to be meaningful, but which generally cannot be checked syntactically. One should in fact know the domain of variable values. The classic solution of runtime tests is generally considered unacceptable because of its cost. Only an automatic semantic analysis of programs can provide an economically profitable solution. <LI> Most of the optimization techniques used in the compilation of programs can only be implemented when the conditions ensuring the equivalence between the transformed program and the original one are satisfied, as well as a real improvement in their performance. When there is a doubt, the classical option is that of considering the most pessimistic hypothesis, but a more in-depth semantic analysis of the program may allow us to avoid this. </UL> Generally, the development of a theory for the semantic analysis of programs leading to automatized applications, is justified by the technical resolution of the software reliability and software efficiency problems. It is, in our opinion, complementary to the efforts, which are currently made to turn the art of programming into the status of a science. <P> Let us now give a very short summary of the content of this thesis: <P> We will reduce the problem of the determination of semantic properties of a program, to the problem of building up the extreme fixed points of monotone operators on a complete lattice. After this introduction, the second chapter is then dedicated to the mathematical study of fixed-point theorems in complete lattices. We provide a constructive demonstration of Tarski's theorem, showing that the set of fixed points of a monotone operator F on a complete lattice L is the image of L by the pre-closures defined by means of transfinite iteration limits. It is a matter of showing how classic iterative methods can be adapted to converge starting from any starting point and also, to reach fixed points other than the least and the greatest one. This also allows us to define the union and the intersection in the lattice of the fixed points of F in a constructive way, that is by recurrences using F. We then obtain, as a particular case, the theorem of construction of the least fixed point of a continuous operator. We will then consider some systems of monotone fixed point equations in a complete lattice. After remembering the formal resolution method by elimination of variables, we will demonstrate a convergence result of chaotic iterative methods, asynchronous and asynchronous with memory. This opens the way to the resolution of systems of monotone equations on a lattice, using different processors, calculating in parallel, without the necessity of any synchronization. <P> In the third chapter, the problem of semantic analysis of programs is studied independently on the problems of language definition, within the very general framework of studying the behavioral of a discrete dynamic system. A program is a discrete dynamic system as long as it defines a transition relation (or a transition function, if it is deterministic), between the states of memory preceding or following the execution of any elementary instruction. To study the behavior of a dynamic discrete system, it is necessary to characterize the set of reachable states satisfying a given entry specification, or else, to characterize the set of ascendants satisfying a given exit specification. In other words, it is necessary to determine the weakest pre-condition, regarding the entry states, so that the system may evolve towards a state satisfying a given postcondition, or the strongest post-condition characterizing the states towards which the system evolves, starting from any entry state, satisfying a given pre-condition. We will show that these conditions are obtained as solutions of fixed-points equations or of equation systems, when the set of states of the dynamic discrete system is partitioned. We will then formalize the operational semantics of a simple programming language, corresponding to sequential iterative programs, and we will show how a program defines a discrete dynamic system. We will then apply the results obtained by the analysis of discrete dynamic systems behavior to the semantic analysis of programs. This leads us to define forward and backward deductive semantics of programs, generalizing the classic forward program verification method of Floyd-Naur, and the backward method of Hoare-Dijkstra, to techniques for formalizing the semantics of programming languages. In fact, the forward and backwards deductive semantics define the conditions in which a program is correctly carried out, is not carried out at all, or leads to an error as a solution of semantic equation systems, associated to the program. Both semantics can be used to characterize, in each point of the program, the set of descendants of the entry states and the set of ascendants of the exit states. As a consequence, they are equivalent, as both allow to make an exact semantic analysis of programs. <P> After having shown that the exact semantic analysis of programs consists in solving equation systems, keeping in mind that the solutions to these equations are not automatically computable, and wishing, at the same time, to find some automatic techniques of semantic analysis of programs, we are forced to limit ourselves to approximate automatic analyses of programs. So in chapter four we will study some calculation methods for approximating fixed points of monotone operators on a lattice. To effectively calculate lower and upper approximations of the solutions of an equation system, we essentially propose two complementary methods. They consist, on one end, in simplifying the equations to solve and, on the other end, in accelerating the convergence of iterative methods of fixed-point construction. To accelerate the convergence of an iteration which does not stabilize itself naturally in a fixed number of steps, we propose to extrapolate, while calculating the terms of the sequence of iterates to obtain an approximation of its limit in a finite number of steps. As in iterative methods with convergence acceleration, the simplification of equations is widely used in numerical analysis but, for what our problems need, we have to study them in a purely algebraic framework. To simplify the semantic equation systems associated to the programs, for each particular problem of semantic analysis of programs, we propose to ignore a priori certain properties and only keep the program properties which are meaningful for this specific application. From an algebraic viewpoint, this approximation is formalized by a closure in the domain of the equations to solve, a closure that we will define, in an equivalent way, by a Moore family, as relations of congruence, or pairs of adjoint functions. Different approximate analyses can be combined by combining the corresponding closures, and in particular the lattice of closures formalizes the creation of a hierarchy of approximations, depending on their precision. <P> In chapter five we will develop automatic semantic programs analysis methods, therefore necessarily approximate. In order to perform an approximate semantic analysis of programs, we propose to compute an approximation of the forward and backward systems of semantic equations associated to this program. Having chosen a particular class of program properties providing useful answers to a given problem, we will show how the results of chapter four allows us to design an algorithm which can automatically carry out the analysis of any program for this class of properties. The design of this algorithm is based on the choice of a closure allowing to define a space of approximate properties, as well as the rules of construction of systems of simplified equation systems associated to a program. To solve these equations, we will use an iterative method. Extrapolation operations will also have to be designed when conver gence must be accelerated. We will illustrate our approach by giving some examples of the conception of an approximate semantic analysis of programs. After having briefly examined many different classic examples within program optimization, we will deal with some applications to the discovery of pointers properties, the determination of the types of variables in high level languages without declarations, the analysis of the interval of values of numeric variables, and also to the discovery of linear relations of equality or inequality between the variables of a program. <P> Chapter six deals with recursive procedures, whose analysis is more complex than the one of sequential iterative programs, given that it is necessary to consider functional equations of the form f(x) = F(f)(x), and not equations of the type x = f(x), any more. We will use the same approach as for iterative sequential programs, by defining a deductive semantics, then, by introducing some approximation methods which, in fact, generalize the study of chapter four in the case of functional equation systems.

Abstract: It is shown that the class of asynchronous iterative methods and asynchronous iterative methods with memory can be used to solve a fixed point of monotone equations in a complete lattice. The rather technical proofs use no additional hypotheses (such as continuity or chain conditions). These iterative methods correspond to a parallel algorithm for solving the system of equations on a multiprocessor system with no synchronization between cooperating processes.