In numerical analysis, error propagation refers to how small inaccuracies in input data or intermediate computations accumulate and affect the final result, typically governed by the stability and sensitivity of the algorithm with respect to some perturbations. The definition of a similar concept in approximated program analysis is still a challenge. In abstract interpretation, inaccuracy arises from the abstraction itself, and the propagation of this error is dictated by the abstract interpreter. In most cases, such imprecision is inevitable. In this paper we introduce a logic for deriving (upper) bounds on the inaccuracy of an abstract interpretation. We are able to derive a function that bounds the imprecision of the result of an abstract interpreter from the imprecision of its input data. When this holds we have what we call partial local completeness of the abstract interpreter, a weaker form of completeness known in the literature. To this end, we introduce the notion of a generator for a property represented in the abstract domain. Generators allow us to restrict the search space when verifying whether the bounding function holds for a given program and input. We then introduce a program logic, called Error Propagation Logic (EPL), for propagating the error bounds produced by an abstract interpretation. This logic is a combination of correctness and incorrectness logics and a logic for program ω - continuity that is also introduced in this paper.

We study “ the best of abstract interpretations ”, that is, the best possible abstract interpretations of programs. Abstract interpretations are inductively defined by composing abstract transfer functions for the basic commands, such as assignments and Boolean guards. However, abstract interpretation is not compositional: even if the abstract transfer functions of the basic commands are the best possible ones on a given abstract domain A this does not imply that the whole inductive abstract interpretation of a program p is still the best in A . When this happens we are in the optimal scenario where the abstract interpretation of p coincides with the abstraction of the concrete interpretation of p . Our main contributions are threefold. Firstly, we investigate the computability properties of the class of programs having the best possible abstract interpretation on a fixed abstract domain A . We show that this class is, in general, not straightforward and not recursive. Secondly, we prove the impossibility of achieving the best possible abstract interpretation of any program p either by an effective compilation of p or by minimally refining or simplifying the abstract domain A . These results show that the program property of having the best possible abstract interpretation is not trivial and, in general, hard to achieve. We then show how to prove that the abstract interpretation of a program is indeed the best possible one. To this aim, we put forward a program logic parameterized on an abstract domain A which infers triples p r e ] A p p o s t ] A . These triples encode that the inductive abstract interpretation of p on A with abstract input p r e ∈ A gives p o s t ∈ A as abstract output and this is the best possible in A .

It is widely known that the precision of a program analyzer is closely related to intensional program properties, namely, properties concerning how the program is written. This explains, for instance, the interest in code obfuscation techniques, namely, tools explicitly designed to degrade the results of program analysis by operating syntactic program transformations. Less is known about a possible relation between what the program extensionally computes, namely, its input-output relation, and the precision of a program analyzer. In this paper we explore this potential connection in an effort to isolate program fragments that can be precisely analyzed by abstract interpretation, namely, programs for which there exists a complete abstract interpretation. In the field of static inference of numeric invariants, this happens for programs, or parts of programs, that manifest a monotone (either non-decreasing or non-increasing) behavior. We first formalize the notion of program monotonicity with respect to a given input and a set of numerical variables of interest. A sound proof system is then introduced with judgments specifying whether a program is monotone relatively to a set of variables and a set of inputs. The interest in monotonicity is justified because we prove that the family of monotone programs admits a complete abstract interpretation over a specific class of non-trivial numerical abstractions and inputs. This class includes all non-relational abstract domains that refine interval analysis (i.e., at least as precise as the intervals abstraction) and that satisfy a topological convexity hypothesis.

Robustness is a key and desirable property of any classifying system, in particular, to avoid the ever-rising threat of adversarial attacks. Informally, a classification system is robust when the result is not affected by the perturbation of the input. This notion has been extensively studied, but little attention has been dedicated to how the perturbation affects the classification. The interference between perturbation and classification can manifest in many different ways, and its understanding is the main contribution of the present article. Starting from a rigorous definition of a standard notion of robustness, we build a formal method for accommodating the required degree of robustness—depending on the amount of error the analyst may accept on the classification result. Our idea is to precisely model this error as an abstraction . This leads us to define weakened forms of robustness also in the context of programming languages, particularly in language-based security, e.g., information-flow policies, and in program verification. The latter is possible by moving from a quantitative (standard) model of perturbation to a novel qualitative model, given by means of the notion of abstraction. As in language-based security, we show that it is possible to confine adversities, which means to characterize the degree of perturbation (and/or the degree of class generalization) for which the classifier may be deemed adequately robust. We conclude with an experimental evaluation of our ideas, showing how weakened forms of robustness apply to state-of-the-art image classifiers.

Abstract interpretation is a well-known and extensively used method to extract over-approximate program invariants by a sound program analysis algorithm. Soundness means that no program errors are lost and it is, in principle, guaranteed by construction. Completeness means that the abstract interpreter reports no false alarms for all possible inputs, but this is extremely rare because it needs a very precise analysis. We introduce a weaker notion of completeness, called local completeness , which requires that no false alarms are produced only relatively to some fixed program inputs. Based on this idea, we introduce a program logic, called Local Completeness Logic for an abstract domain A , for proving both the correctness and incorrectness of program specifications. Our proof system, which is parameterized by an abstract domain A , combines over- and under-approximating reasoning. In a provable triple ⊦ A [ p ] 𝖼 [ q ], 𝖼 is a program, q is an under-approximation of the strongest post-condition of 𝖼 on input p such that their abstractions in A coincide. This means that q is never too coarse, namely, under some mild assumptions, the abstract interpretation of 𝖼 does not yield false alarms for the input p iff q has no alarm . Therefore, proving ⊦ A [ p ] 𝖼 [ q ] not only ensures that all the alarms raised in q are true ones, but also that if q does not raise alarms, then 𝖼 is correct. We also prove that if A is the straightforward abstraction making all program properties equivalent, then our program logic coincides with O’Hearn’s incorrectness logic, while for any other abstraction, contrary to the case of incorrectness logic, our logic can also establish program correctness.

Abstract interpretation is a sound-by-construction method for program verification: any erroneous program will raise some alarm. However, the verification of correct programs may yield false-alarms, namely it may be incomplete. Ideally, one would like to perform the analysis on the most abstract domain that is precise enough to avoid false-alarms. We show how to exploit a weaker notion of completeness, called local completeness, to optimally refine abstract domains and thus enhance the precision of program verification. Our main result establishes necessary and sufficient conditions for the existence of an optimal, locally complete refinement, called pointed shell. On top of this, we define two repair strategies to remove all false-alarms along a given abstract computation: the first proceeds forward, along with the concrete computation, while the second moves backward within the abstract computation. Our results pave the way for a novel modus operandi for automating program verification that we call Abstract Interpretation Repair (AIR): instead of choosing beforehand the right abstract domain, we can start in any abstract domain and progressively repair its local incompleteness as needed. In this regard, AIR is for abstract interpretation what CEGAR is for abstract model checking.

Imprecision is inherent in any decidable (sound) approximation of undecidable program properties. In abstract interpretation this corresponds to the release of false alarms, e.g., when it is used for program analysis and program verification. As all alarming systems, a program analysis tool is credible when few false alarms are reported. As a consequence, we have to live together with false alarms, but also we need methods to control them. As for all approximation methods, also for abstract interpretation we need to estimate the accumulated imprecision during program analysis. In this paper we introduce a theory for estimating the error propagation in abstract interpretation, and hence in program analysis. We enrich abstract domains with a weakening of a metric distance. This enriched structure keeps coherence between the standard partial order relating approximated objects by their relative precision and the effective error made in this approximation. An abstract interpretation is precise when it is complete. We introduce the notion of partial completeness as a weakening of precision. In partial completeness the abstract interpreter may produce a bounded number of false alarms. We prove the key recursive properties of the class of programs for which an abstract interpreter is partially complete with a given bound of imprecision. Then, we introduce a proof system for estimating an upper bound of the error accumulated by the abstract interpreter during program analysis. Our framework is general enough to be instantiated to most known metrics for abstract domains.

We introduce the notion of local completeness in abstract interpretation and define a logic for proving both the correctness and incorrectness of some program specification. Abstract interpretation is extensively used to design sound-by-construction program analyses that over-approximate program behaviours. Completeness of an abstract interpretation A for all possible programs and inputs would be an ideal situation for verifying correctness specifications, because the analysis can be done compositionally and no false alert will arise. Our first result shows that the class of programs whose abstract analysis on A is complete for all inputs has a severely limited expressiveness. A novel notion of local completeness weakens the above requirements by considering only some specific, rather than all, program inputs and thus finds wider applicability. In fact, our main contribution is the design of a proof system, parameterized by an abstraction A, that, for the first time, combines over- and under-approximations of program behaviours. Thanks to local completeness, in a provable triple ⊢A [P ] c [Q], the assertion Q is an under-approximation of the strongest post-condition post[c](P ) such that the abstractions in A of Q and post[c](P ) coincide. This means that Q is never too coarse, namely, under mild assumptions, the abstract interpretation of c does not yield false alerts for the input P iff Q has no alert. Thus, ⊢ A [P ] c [Q] not only ensures that all the alerts raised in Q are true ones, but also that if Q does not raise alerts then c is correct.

In this paper we generalise the notion of extensional (functional) equivalence of programs to abstract equivalences induced by abstract interpretations . The standard notion of extensional equivalence is recovered as the special case, induced by the concrete interpretation. Some properties of the extensional equivalence, such as the one spelled out in Rice’s theorem, lift to the abstract equivalences in suitably generalised forms. On the other hand, the generalised framework gives rise to interesting and important new properties, and allows refined, non-extensional analyses. In particular, since programs turn out to be extensionally equivalent if and only if they are equivalent just for the concrete interpretation, it follows that any non-trivial abstract interpretation uncovers some intensional aspect of programs. This striking result is also effective, in the sense that it allows constructing, for any non-trivial abstraction, a pair of programs that are extensionally equivalent, but have different abstract semantics. The construction is based on the fact that abstract interpretations are always sound, but that they can be made incomplete through suitable code transformations. To construct these transformations, we introduce a novel technique for building incompleteness cliques of extensionally equivalent yet abstractly distinguishable programs: They are built together with abstract interpretations that produce false alarms. While programs are forced into incompleteness cliques using both control-flow and data-flow transformations, the main result follows from limitations of data-flow transformations with respect to control-flow ones. A further consequence is that the class of incomplete programs for a non-trivial abstraction is Turing complete. The obtained results also shed a new light on the relation between the techniques of code obfuscation and the precision in program analysis.

The fundamental idea of Abstract 2 Interpretation (A 2 I), also called meta-abstract interpretation, is to apply abstract interpretation to abstract interpretation-based static program analyses. A 2 I is generally meant to use abstract interpretation to analyse properties of program analysers. A 2 I can be either offline or online. Offline A 2 I is performed either before the program analysis, such as variable packing used by the Astrée program analyser, or after the program analysis, such as in alarm diagnosis. Online A 2 I is performed during the program analysis, such as Venet’s cofibred domains or Halbwachs et al.’s and Singh et al.’s variable partitioning techniques for fast polyhedra/numerical abstract domains. We formalize offline and online meta-abstract interpretation and illustrate this notion with the design of widenings and the decomposition of relational abstract domains to speed-up program analyses. This shows how novel static analyses can be extracted as meta-abstract interpretations to design efficient and precise program analysis algorithms.

We study from a computability perspective static program analysis, namely detecting sound program assertions, and verification, namely sound checking of program assertions. We first design a general computability model for domains of program assertions and corresponding program analysers and verifiers. Next, we formalize and prove an instantiation of Rice’s theorem for static program analysis and verification. Then, within this general model, we provide and show a precise statement of the popular belief that program analysis is a harder problem than program verification: we prove that for finite domains of program assertions, program analysis and verification are equivalent problems, while for infinite domains, program analysis is strictly harder than verification.

Abstract interpretation is a method to automatically find invariants of programs or pieces of code whose semantics is given via least fixed-points. Up-to techniques have been introduced as enhancements of coinduction, an abstract principle to prove properties expressed via greatest fixed-points.

Abstract Code protection technologies require anti reverse engineering transformations to obfuscate programs in such a way that tools and methods for program analysis become ineffective. We introduce the concept of model deformation inducing an effective code obfuscation against attacks performed by abstract model checking. This means complicating the model in such a way a high number of spurious traces are generated in any formal verification of the property to disclose about the system under attack.We transform the program model in order to make the removal of spurious counterexamples by abstraction refinement maximally inefficient. Because our approach is intended to defeat the fundamental abstraction refinement strategy, we are independent from the specific attack carried out by abstract model checking. A measure of the quality of the obfuscation obtained by model deformation is given together with a corresponding best obfuscation strategy for abstract model checking based on partition refinement.

In this paper we generalize the notion of non-interference making it parametric relatively to what an attacker can analyze about the input/output information flow. The idea is to consider attackers as data-flow analyzers, whose task is to reveal properties of confidential resources by analyzing public ones. This means that no unauthorized flow of information is possible from confidential to public data, relatively to the degree of precision of an attacker. We prove that this notion can be fully specified in standard abstract interpretation framework, making the degree of security of a program a property of its semantics. This provides a comprehensive account of non-interference features for language-based security. We introduce systematic methods for extracting attackers from programs, providing domain-theoretic characterizations of the most precise attackers which cannot violate the security of a given program. These methods allow us both to compare attackers and program secrecy by comparing the corresponding abstractions in the lattice of abstract interpretations, and to design automatic program certification tools for language-based security by abstract interpretation.

Abstract Obfuscation is the art of making code hard to reverse engineer and understand. In this paper, we propose a formal model for specifying and understanding the strength of obfuscating transformations with respect to a given attack model. The idea is to consider the attacker as an abstract interpreter willing to extract information about the program’s semantics. In this scenario, we show that obfuscating code is making the analysis imprecise, namely making the corresponding abstract domain incomplete. It is known that completeness is a property of the abstract domain and the program to analyse. We introduce a framework for transforming abstract domains, i.e., analyses, towards incompleteness. The family of incomplete abstractions for a given program provides a characterisation of the potency of obfuscation employed in that program, i.e., its strength against the attack specified by those abstractions. We show this characterisation for known obfuscating transformations used to inhibit program slicing and automated disassembly.

Completeness is a key feature of abstract interpretation. It corresponds to exactness of the abstraction of fix-points and relies upon the need of absence of false alarms in static program analysis. Making abstract interpretation complete is therefore a major problem in approximating the semantics of programming languages. In this paper, we consider the problem of making abstract interpretations complete by minimally modifying the predicate transformer, i.e. the semantics, of a program. We study the mathematical properties of complete functions on complete lattices and prove the existence of minimal transformations of monotone functions to achieve completeness. We then apply minimal complete transformers to prove the minimality of standard program transformations in security, such as static program monitoring.

We want to prove that a static analysis of a given program is complete, namely, no imprecision arises when asking some query on the program behavior in the concrete (ie, for its concrete semantics) or in the abstract (ie, for its abstract interpretation). Completeness proofs are therefore useful to assign confidence to alarms raised by static analyses. We introduce the completeness class of an abstraction as the set of all programs for which the abstraction is complete. Our first result shows that for any nontrivial abstraction, its completeness class is not recursively enumerable. We then introduce a stratified deductive system to prove the completeness of program analyses over an abstract domain A. We prove the soundness of the deductive system. We observe that the only sources of incompleteness are assignments and Boolean tests --- unlikely a common belief in static analysis, joins do not induce incompleteness. The first layer of this proof system is generic, abstraction-agnostic, and it deals with the standard constructs for program composition, that is, sequential composition, branching and guarded iteration. The second layer is instead abstraction-specific: the designer of an abstract domain A provides conditions for completeness in A of assignments and Boolean tests which have to be checked by a suitable static analysis or assumed in the completeness proof as hypotheses. We instantiate the second layer of this proof system first with a generic nonrelational abstraction in order to provide a sound rule for the completeness of assignments. Orthogonally, we instantiate it to the numerical abstract domains of Intervals and Octagons, providing necessary and sufficient conditions for the completeness of their Boolean tests and of assignments for Octagons.

We introduce a model for mixed syntactic/semantic approximation of programs based on symbolic finite automata (SFA). The edges of SFA are labeled by predicates whose semantics specifies the denotations that are allowed by the edge. We introduce the notion of abstract symbolic finite automaton (ASFA) where approximation is made by abstract interpretation of symbolic finite automata, acting both at syntactic (predicate) and semantic (denotation) level. We investigate in the details how the syntactic and semantic abstractions of SFA relate to each other and contribute to the determination of the recognized language. Then we introduce a family of transformations for simplifying ASFA. We apply this model to prove properties of commonly used tools for similarity analysis of binary executables. Following the structure of their control flow graphs, disassembled binary executables are represented as (concrete) SFA, where states are program points and predicates represent the (possibly infinite) I/O semantics of each basic block in a constraint form. Known tools for binary code analysis are viewed as specific choices of symbolic and semantic abstractions in our framework, making symbolic finite automata and their abstract interpretations a unifying model for comparing and reasoning about soundness and completeness of analyses of low-level code.

In this extended abstract we survey the most recent developments in code obfuscation and protection from a programming languages perspective. Starting from known impossibility results on universal and general purpose code obfuscation, we show that provably secure obfuscation can be achieved by constraining the attack model. This corresponds to associate attacks with suitable forms of interpretation. In this context it is always possible to systematically making code obscure, making this interpretation failing in extracting (attacking) code. The code transformation can itself be specified as the specialization of a distorted interpreter.

How to construct a general program obfuscator? We present a novel approach to automatically generating obfuscated code P2 from any program P whose source code is given. Start with a (program-executing) interpreter interp for the language in which P is written. Then "distort" interp so it is still correct, but its specialization P2 w.r.t. P is transformed code that is equivalent to the original program, but harder to understand or analyze. Potency of the obfuscator is proved with respect to a general model of the attacker, modeled as an approximate (abstract) interpreter. A systematic approach to distortion is to make program P obscure by transforming it to P2 on which (abstract) interpretation is incomplete. Interpreter distortion can be done by making residual in the specialization process sufficiently many interpreter operations to defeat an attacker in extracting sensible information from transformed code. Our method is applied to: code flattening, data-type obfuscation, and opaque predicate insertion. The technique is language independent and can be exploited for designing obfuscating compilers.

Reliable and secure system design requires an increasing number of methods, algorithms, and tools for automatic program manipulation. Any program change corresponds to a transformation that affects the semantics at some given level of abstraction. We call these techniques model deformations. In this paper we propose a mathematical foundation for completeness-driven deformations of transition systems w.r.t. a given abstraction, and we introduce an algorithm for systematic deformation of Kripke structures for inducing strong preservation in abstract model checking. We prove that our model deformations are deeply related with must and may transitions in modal transition systems.

Interference and dependence are closely related concepts: interference being the observable phenomenon connected with dependence. Essentially, interference means that the behaviour of some parts of a dynamic system may influence the behaviour of other parts of the same system, while dependence specifies how the semantics of sub-components of a dynamic system are related. Identifying, measuring and controlling interference is essential in many aspects of modern computer science, in particular, in security, program analysis and verification, debugging, systems specification, model checking, program manipulation, program slicing, reverse engineering, data mining, distributed databases and systems biology. In all these fields, dependency and interference play a key role in designing suitable abstractions or in partitioning complex systems into simpler ones. Reasoning about dependency and interference requires theories, models and semantics, as well as algorithms and tools for their analysis. Beginning in 2004, the series of Programming Language Interference and Dependence (PLID) workshops has been devoted to promoting and spreading cutting-edge research in this field, with a particular emphasis on unpublished results with great impact on the theoretical basis. PLID2007, which was held at the The Technical University of Denmark on 21 August 2007, was particularly successful, and constituted the ideal forum for announcing a call for papers for a special journal issue on programming language interference and dependence, which would not necessarily be restricted to PLID2007 contributions. From the many expressions of interest, we selected six contributions by leading researchers in the field, some of which had been presented at the PLID2007 workshop. The selected papers focus on foundational aspects of dependency and interference, with applications in language-based security, data-base management systems and program slicing.

Completeness in abstract interpretation models the ideal situation where no loss of precision is introduced in computations by approximating concrete data by their abstractions. If we interpret the abstraction as the ability of an attacker to distinguish, i.e., observe, properties of public computations, and the computation as the concrete denotational semantics of the program, then the lack of precision, encoded in abstract interpretation as a lack of completeness, corresponds precisely to the leakage of information corresponding to a violated security policy. This correspondence allows us to inherit, in the field of language-based security, the whole theory and methodology for making abstract domains complete. In particular, we prove that an adjoint relation exists between the power of the attacker and the amount of the information released – the more the attacker can observe, the less information can be kept private. This characterisation is achieved by interpreting, in the security context, the standard adjoint transformations making an abstract domain complete by refining and simplifying abstractions.

Questo rapporto è disponibile su Web all’indirizzo: This report is available on the web at the address:

In recent years code obfuscation has attracted research interest as a promising technique for protecting secret properties of programs. The basic idea of code obfuscation is to transform programs in order to hide their sensitive information while preserving their functionality. One of the major drawbacks of code obfuscation is the lack of a rigorous theoretical framework that makes it difficult to formally analyze and certify the effectiveness of obfuscating techniques. We face this problem by providing a formal framework for code obfuscation based on abstract interpretation and program semantics. In particular, we show that what is hidden and what is preserved by an obfuscating transformation can be expressed as abstract interpretations of program semantics. Being able to specify what is masked and what is preserved by an obfuscation allows us to understand its potency, namely the amount of obscurity that the transformation adds to programs. In the proposed framework, obfuscation and attackers are modeled as approximations of program semantics and the lattice of abstract interpretations provides a formal tool for comparing obfuscations with respect to their potency. In particular, we prove that our framework provides an adequate setting to measure not only the potency of an obfuscation but also its resilience, i.e., the difficulty of undoing the obfuscation. We consider code obfuscation by opaque predicate insertion and we show how the degree of abstraction needed to disclose different opaque predicates allows us to compare their potency and resilience.

In this tutorial we will consider abstract non-interference as a formal model for reasoning about language based security. Abstract non-interference generalises standard non-interference by modelling the information leaked as abstract properties of concrete computations. In this case abstractions model both the observational capabilities of attackers and the amount of information that may flow between program components, e.g., from private to public variables, dynamically at run-time. We prove that abstract non-interference generalizes known models of attackers in language-based security and provides at the same time a formal setting for comparing many of the known approaches for weakening non-interference. We introduce a proof system for checking abstract non-interference and systematic methods, i.e., abstraction transformers, for deriving the most concrete harmless attacker for which a program is secure together with the corresponding maximal amount of information released. This provides the possibility of associating programs with canonical attackers and compare them according to their relative degree of security in the lattice of abstract interpretations. Due to its semantic-based approach and the generality of abstract interpretation and non-interference notions, abstract non-interference can be fairly considered as a unifying theory for understanding and reasoning about information-flow in programming languages, including security, program slicing and dependence analysis as special cases.

In this paper we show how abstract interpretation, and more specifically completeness, provides an adequate model for reasoning about code obfuscation and watermarking. The idea is that making a program obscure, or equivalently hiding information in it, corresponds to force an interpreter (the attacker) to become incomplete in its attempts to extract information about the program. Here abstract interpretation provides the model of the attacker (malicious host) and abstract interpretation transformers provide driving methods for understanding and designing new obfuscation and watermarking strategies: Obfuscation corresponds to make the malicious host incomplete and watermarking corresponds to hide secrets where incomplete attackers cannot extract them unless some secret key is given.

Control code obfuscation is intended to prevent malicious reverse engineering of software by masking the program control flow. These obfuscating transformations often rely on the existence of opaque predicates, that support the design of transformations that break up the program control flow. We prove that an algorithm for control obfuscation by opaque predicate insertion can be systematically derived as an abstraction of a suitable semantic transformation. In this framework, deobfuscation is interpreted as an attacker which can observe the computational behaviour of programs up to a given precision degree. Both obfuscation and deobfuscation can therefore be interpreted as approximations of program semantics, where approximation is formalized using abstract interpretation theory. In particular we prove that abstract interpretation provides the adequate setting to measure the potency of an obfuscation algorithm by comparing the degree of abstraction of the most abstract domains which are able to disclose opaque predicates.

In this article, we show that reversible analyses of logic languages by abstract interpretation can be performed without loss of precision by systematically refining abstract domains. This is obtained by adding to the abstract domain the minimal amount of concrete semantic information so that this refined abstract domain becomes rich enough to allow goal-driven and goal-independent analyses agree. These domains are known as condensing abstract domains. Essentially, an abstract domain A is condensing when the goal-driven analysis performed on A for a program P and a given query can be retrieved with no loss of precision from the goal-independent analysis on A of P . We show that condensation is an abstract domain property and that the problem of making an abstract domain condensing boils down to the problem of making the corresponding abstract interpretation complete, in a weakened form, with respect to unification. In the case of abstract domains for logic program analysis approximating computed answer substitutions, we provide a clean logical characterization of condensing domains as fragments of propositional linear logic. We apply our methodology to the systematic design of condensing domains for freeness and independence analysis.

In this paper we study the connection between the structure of relational abstract domains for program analysis and compositionality of the underlying semantics. Both can be systematically designed as solution of the same abstract domain equation involving the same domain refinement: the reduced power operation. We prove that most well-known compositional semantics of imperative programs, such as the standard denotational and weakest precondition semantics can be systematically derived as solutions of simple abstract domain equations. This provides an equational presentation of both semantics and abstract domains for program analysis in a unique formal setting. Moreover both finite and transfinite compositional semantics share the same structure, and this allows us to provide consistent models for program manipulation. Categories and Subject Descriptors D.3 [Programming languages]: Formal definitions and theory---Semantics; F.3 [Logics and meanings of programs ]: Semantics of Programming Languages---algebraic approaches to semantics, denotational semantics, operational semantics General Terms Theory, Verification Keywords Abstract interpretation, reduced power, compositional semantics, transfinite semantics, program manipulation. 1.

We characterize the symmetric structure of Cousot's hierarchy of semantics in terms of a purely algebraic manipulation of abstract domains. We consider domain complementation in abstract interpretation as a formal method for systematically deriving complementary semantics of programming languages. We prove that under suitable hypothesis the semantics abstraction commutes with respect to domain complementation. This result allows us to prove that angelic and demonic/innite semantics are complementary and provide a minimal decomposition of all natural-style trace-based, relational, denotational, Dijkstra's predicate transformer and Hoare's axiomatic semantics. We apply this construction to the case of concurrent constraint programming, characterizing well known semantics as abstract interpretation of maximal traces of constraints. Categories and Subject Descriptors D.3 [Programming languages]: Formal denitions and theory|Semantics; F.3 [Logics and meanings of programs ]: Semantics of...

Completeness is an ideal, although uncommon, feature of abstract interpretations, formalizing the intuition that, relatively to the properties encoded by the underlying abstract domains, there is no loss of information accumulated in abstract computations. Thus, complete abstract interpretations can be rightly understood as optimal. We deal with both pointwise completeness, involving generic semantic operations, and (least) fixpoint completeness. Completeness and fixpoint completeness are shown to be properties that depend on the underlying abstract domains only. Our primary goal is then to solve the problem of making abstract interpretations complete by minimally extending or restricting the underlying abstract domains. Under the weak and reasonable hypothesis of dealing with continuous semantic operations, we provide constructive characterizations for the least complete extensions and the greatest complete restrictions of abstract domains. As far as fixpoint completeness is concerned, for merely monotone semantic operators, the greatest restrictions of abstract domains are constructively characterized, while it is shown that the existence of least extensions of abstract domains cannot be, in general, guaranteed, even under strong hypotheses. These methodologies, which in finite settings give rise to effective algorithms, provide advanced formal tools for manipulating and comparing abstract interpretations, useful both in static program analysis and in semantics design. A number of examples illustrating these techniques are given.

We introduce a practical method for abductive analysis of modular logic programs. This is obtained by reversing the deduction process, which is usually applied in static-dataflow analysis of logic programs, on generic. possibly abstract, domains for analysis. The approach is validated in the framework of abstract interpretation. The abduced information provides an abstract specification for program modules which can be of assistance both in top-down development of programs and in compile-time optimization. To the best of our knowledge this is the first application of abductive reasoning in dataflow analysis of logic programs.

In this article we introduce the notion of Heyting completion in abstract interpretation. We prove that Heyting completion provides a model for Cousot's reduced cardinal power of abstract domains and that it supplies a logical basis to specify relational domains for program analysis and abstract interpretation. We study the algebraic properties of Heyting completion in relation with other well-known domain transformers, like reduced product and disjunctive completion. This provides a uniform algebraic setting where complex abstract domains can be specified by simple logic formulas, or as solutions of recursive abstract domain equations, involving few basic operations for domain construction, all characterized by a clean logical interpretation. We apply our framework to characterize directionality and condensing and in downward closed analysis of (constraint) logic programs.

Reduced product of abstract domains is a rather well-known operation for domain composition in abstract interpretation. In this article, we study its inverse operation, introducing a notion of domain complementation in abstract interpretation. Complementation provides as systematic way to design new abstract domains, and it allows to systematically decompose domains. Also, such an operation allows to simplify domain verification problems, and it yields space-saving representations for complex domains. We show that the complement exists in most coses, and we apply complementation to three well-know abstract domains, notably to Cousot and Cousot's interval domain for integer variable analysis, to Cousot and Cousot's domain for comportment analysis of functional languages, and to the domain Sharing for aliasing analysis of logic languages.

This paper describes a semantic basis for a compositional approach to the analysis of logic programs. A logic program is viewed as consisting of a set of modules, each module defining a subset of the program's predicates. Analyses are constructed by considering abstract interpretations of a compositional semantics. The abstract meaning of a module corresponds to its analysis and composition of abstract meanings corresponds to composition of analyses. Such an approach is essential for large program development so that altering one module does not require re-analysis of the entire program. We claim that for a substantial class of programs, compositional analyses which are based on a notion of abstract unfolding provide the same precision as non-compositional analysis. A compositional analysis for ground dependencies is included to illustrate the approach. To the best of our knowledge this is the first account of a compositional framework for the analysis of logic programs.

The goal of this paper is to construct a semantic basis for the abstract interpretation of Prolog programs. Prolog is a well-known logic programming language which applies a depth-first search strategy in order to provide a practical approximation of Horn clause logic. While pure logic programming has clean fixpoint, model-theoretic and operational semantics the situation for Prolog is different. Difficulties in capturing the declarative meaning of Prolog programs have led to various semantic definitions which attempt to encode the search strategy in different mathematical frameworks. However, semantic based analyses of Prolog are typically achieved by abstracting the more simple but less precise declarative semantics of pure logic programs. We propose instead to model Prolog control in a simple constraint logic language which is presented together with its declarative and operational semantics. This enables us to maintain the usual approach to declarative semantics of logic programs while capturing control aspects such as search strategy and selection rule.

The theory of abstract interpretation provides a formal framework to develop advanced dataflow analysis tools. The idea is to define a nonstandard semantics which is able to compute, in finite time, an approximated model of the program. In this paper, we define an abstract interpretation framework based on a fixpoint approach to the semantics. This leads to the definition, by means of a suitable set of operators, of an abstract fixpoint characterization of a model associated with the program. Thus, we obtain a specializable abstract framework for bottom-up abstract interpretations of definite logic programs. The specialization of the framework is shown on two examples, namely, gound-dependence analysis and depth-kanalysis.