RICERCA ITALIANA     

Research program

AIDA - Abstract Interpretation Design and Applications

University Co-ordinator

Università degli Studi di PADOVA - MATEMATICA PURA ED APPLICATA - PADOVA(PD)

Research Unit Leader

Francesco RANZATO

Description

The whole project is organized in WorkPackages (WPs) collecting together theoretical and applicative areas of abstract interpretation. The contributions of the research unit of Padova will be mainly in WP2, WP5, WP6. The research activities are planned as follows.WP2: SecurityThe scientific basis sketched above leads to a number of interesting research directions. Task PD-2.1The above point (Sec-1) hints that it would be interesting to design a pi-calculus static analysis which is able to fully exploit the semantics of the involved operations in order to infer precise information. We plan to investigate this issue in order to extend to the spi-calculus a precise and efficient static analysis for the pi-calculus that we recently put forward [CFG03]. Task PD-2.2As far as the above point (Sec-3) is concerned, we aim at modelling explicitly (namely through a particular process) the most dangerous context for a given protocol. Here the benefit would be that the analysis would not need an ad hoc method for encompassing the interactions with the (most dangerous) context, but it would be sufficient to apply the simple analysis (i.e., without an ad hoc way of encompassing the context) to the term modelling the protocol coupled with the term modelling its most dangerous context.Task PD-2.3The achievements of the previous task 2.2 would also provide a solution to the following problem, which is often neglected. Often, in message exchanges, the fact that the context might itself invent messages in order to confuse the honest principals is not taken appropriately into account. The abstraction typically used to make data-flow analyses of spi-calculus finite (cf. (Sec-2)) often relies on the fact that replication produces copies of terms which are identical or, equivalently, which have the same type. This assumption implies that one may construct regular terms only, which are therefore finitely characterizable. It would be interesting to define abstractions which are less restrictive on this issue and still ensure the termination of the analysis. The pi-calculus analysis in [Fer01] is a good example of this kind of approaches.WP5: ConstraintsWithin this workpackage we plan to study the above abstraction interpretation framework for soft constraints [BCR02] and evaluate its usefulness and convenience, both theoretically and experimentally, for several classes of soft constraints. A first evaluation over fuzzy constraints [DFP93] showed promising results [BPR04]. The research activities will be organized in the following tasks.Task PD-5.1We will analyze the current abstraction methodology for soft constraints by studying the relationship with existing abstraction frameworks for hard constraints. We aim at extending the methodology in [BCR02] by incorporating the most interesting features of other frameworks for abstracting classical constraints. In particular, we will study those extensions which allow to improve the efficiency of a solver without loosing too much information in the abstraction process. Moreover, we will also study and design algorithms for the abstraction of soft constraints based on fixpoint computations.Task PD-5.2We will implement and test the above algorithms over several classes of soft constraints, to assess their practical value. Such classes will possibly contain randomly generated problems and also real-life problems. The classes will vary according to several parameters, among them the structure of soft constraints. The considered classes of constraints will include fuzzy constraints and Max-CSP (where one maximizes the sum of the weights of the constraints), which are the most used and whose features are completely different.WP6: Automatic VerificationTask PD-6.1 If a specification f is not valid on a model M then a model checking-based verification algorithm outputs a counterexample to the validity of f on M. Thus, model checking algorithms running on abstract models output abstract counterexamples. An abstract counterexample for f on an abstract model A may be spurious, i.e. it may be an artificial violation of f caused by the approximated abstract model A which does not correspond to any real counterexample on the concrete model M. Clarke et al. [CFHKQST03, CGJLV00, CGJLV03, CJLV02] put forward a spurious counterexample-guided refinement technique for abstract models: they designed an algorithm which is able to test whether a counterexample T yielded by a model checker running on a classical abstract model A -- that is, a state partition -- is spurious and an algorithm which refines A and thus removes the spurious counterexample T. This spurious counterexample-based refinement methodology turns out to be complete for a fragment of ACTL*. Clarke at al. showed experimentally the usefulness of this technique on a number of complex case studies. The goal of this task is to exploit the abstract interpretation-based approach in [RT04a] in order to extend the counterexample-guided refinement methodology to generic abstract models -- not necessarily state partitions -- specified through abstract interpretation and to generic inductively defined languages (possibly different from the fragment of ACTL* in [CGJLV03]). In particular, we aim at studying a notion of spurious counterexample for generic abstract models and hence an algorithm which is able to test whether one such counterexample is spurious.Task PD-6.2 The Paige-Tarjan [PT87] algorithm works by iterating the following basic operation: a current state partition Q is replaced by a refined partition Q' which is obtained from Q by substituting a block B of Q with a pair of sub-blocks B1 and B2. In abstract interpretation terms this operation can be viewed as a "compression" of the current abstract domain w.r.t. set-union [RT04b]. The generalized Paige-Tarjan algorithm which refines abstract models in order to make them strongly preserving w.r.t. some language L relies on the existence of some abstract domain compressor. Unfortunately, compressors rarely exist. However, it is possible to lift the complete domain refinement techniques in [GRS00] one level up, i.e. to higher-orders, in order to apply them to transform mere simplification operators into compressors. The objective of this task is to apply such a methodology in order to define new compression operators (possibly different from the set-union compressor à la Paige-Tarjan) that can be integrated into the generalized Paige-Tarjan algorithm [RT04b].Task PD-6.3 The above techniques allow to get strong preservation of abstract model checking w.r.t. some language L through a refinement of the underlying abstract model. This task instead aims at approaching this same problem under a different perspective. Let A be an abstract model which is not strongly preserving for a language L. Let us assume that L is an inductively defined language, i.e. that L is generated by closing atomic propositions under applications of a set Op of logical/temporal operators (e.g. AND, EX, AX, etc.). The operators generating some language can be compared w.r.t. their precision: if f1:Pow(State)^n Pow(State) and f2:Pow(State)^m Pow(State) are the semantic state interpretations of a pair of logical/temporal operators then f1 f2 can be, for example, defined pointwise. The idea is that of systematically modifying (through refinements or simplifications) the operators in Op defining the language L in order to obtain a language L' such that the abstract model checking on A is strongly preserving for L'. By exploiting the results in [RT04a] this goal can be translated in the following problem in abstract interpretation: given an abstract domain A and a semantic operation f, here the goal is that of refining/simplifying f in a minimal way to f' -- for instance, w.r.t. the pointwise ordering between operations -- so that A becomes complete w.r.t. f'. Thus, from an abstract model checking view this would allow to minimally modify the specification language instead of the abstract model in order to achieve strong preservation.