Research program
AIDA - Abstract Interpretation Design and Applications
University Co-ordinator
Università degli Studi di BOLOGNA -
SCIENZE DELL'INFORMAZIONE - BOLOGNA(BO)
Research Unit Leader
Maurizio GABBRIELLI
Description
The main focus of the research in our unit is on the study of analysis and verification techniques for object-oriented and multithreaded programs (for example Java programs). We will look at this problem from different perspectives mainly using abstract interpretation, constraints and compositional methods. We intend also to investigate the analysis of (constraint) logic programming and declarative languages by using suitable collecting semantics. Thus the activity of the unit of Bologna is relevant for the workpackages 1, 5 and 6 of the project. Specifically, referring to the general workpackages structure of the project, we identify the following research directions for the work of the Bologna unit. Workpackage 1 "Static Analysis" Task Bo.1.1: "Abstract interpretation for object-oriented programs".Type systems and type inference algorithms are the classical methods for static analysis of dynamic properties of programs [Car97]. However, in many papers that propose abstract interpretation techniques to perform static analysis on programming languages, it is shown that often the analyses based on typing rules on the constructs of a language are too rigid and that impose correctness assumptions that could be relaxed. This claim is supported also by the fact that type systems and/or type inference algorithms often can be redefined as abstract semantics or abstract interpreters [Cou97]. To statically check dynamic properties, an abstract interpreter executes a program abstracting the actual values of the variables into elements of a suitable abstract domain. The terminating abstract computation can be viewed as an approximation of the set of all computations of the program. Due to these characteristics, in many cases abstract interpretation can be more precise, in the sense that allows a correct certification of more programs, than type-based analysis.Following this idea, our objective is to define abstract interpretation frameworks improving existing type-based static analyses or introducing new ones. More precisely we consider the following specific objectives.Obj 1.1.1 We want to define abstract interpretation frameworks improving the existing type-based static analyses or introducing new ones. In particular, we aim to define a framework for static analysis of Java bytecode programs. This framework should be based on a formalization of the semantics of bytecode programs and on the consequent abstract interpretation that uses suitable abstract domains. An interesting application, for its aspects of security and mobility, could be the verification of an untrusted bytecode programs against security properties, as well as the analysis already performed by the bytecode verifier. Obj 1.1.2 Using abstract interpretation, we plan to introduce new static analyses, or improve existing ones, that regard more closely concurrent aspects of object oriented formalisms. We will use, as basic formalisms, concurrent object oriented calculi. An example of a work in this task is the enhancement of existing analyses that checks the absence of race conditions in concurrent accesses to an object by several processes.Obj 1.1.3 We have introduced a notion of timed non-interference for real-time systems modeled by timed automata.This notion is suitable to detect interference due to the frequency of certain actions and can be used, forinstance, to analyze the strength of network components against timed attacks. Unfortunately, the most naturalnotion of timed non-interference is undecidable. We aim to use abstract interpretation to define implementable approximate notions leading to the development of tools. Task Bo.1.2: "Analysis of declarative languages based on collecting semantics" Obj 1.2.1 We want to provide an algebraic characterization of what the collecting semantics is. The only work we know on this subject is [Nie88]. As an example of the kind of results we would like to obtain, assume we fix a standard semantics and a property of the observables we are interested in (for example, the monotonicity of the abstraction function w.r.t. the computational ordering). In this case, we may derive a particular collecting semantics as the initial semantics among those which make possible to carry on the analysis in the framework of Galois connections.Obj 1.2.2 We are also looking for a new semantics which is built from the ground up to be more precise than goal-dependent and goal-independent semantics for all the abstract domains. The benefits of this result would be the availability of an unique semantics for all the kind of analysis over logic programs. We also think that it would lead to a deeper understanding of the way abstract domains are built, expecially of the way in which they could be decomposed in a upward-closed and a downward-closed part.Obj 1.2.3 We plan to study optimal algorithms for abstract unification and matching of both substitutions and constraints. We are particularly interested in abstract domains for aliasing and sharing analysis, whose goal is the automatic parallelization of (constraint) logic programs [MH92]. We plan to implement a set of new domains, already introduced in [AS03], and to study the way asbtract matching may be applied in fields like term rewriting systems or functional languages.Part of the research performed in the tasks Bo.1.1 and Bo.1.2 will be done in collaboration with the research unit of Pisa. Workpackage 5: "Constraints" Task Bo.5.1: "Compositional Contraints-based analysis of multithreaded programs" In this subtask we plan to investigate the combined application of abstract interpretation and constraint programming for the analysis and verification of multithreaded software programs. To scale up on practical examples, it is critical to study how to extract abstract models from programs and how to perform analysis compositionally. Thus, our goals are as follows:Obj 5.1.1 Starting from "abstract models" of multithreaded programs (specified in process algebra-like formalisms), we will study the foundations of "compositional verification techniques based on constraints''. The key idea here is to exploit the "compositionality" of constraint operations in order to modularly specify analyses of concurrent systems. Specifically, we will first study how to define a semantic which assign to a process (of a suitable process algebra) a denotation based on constraints; the key issue here is that the syntactic operators of the language (e.g. parallel composition, restriction etc.) should be modeled by means of semantic operators on constraints (e.g. conjunction, existential quantification etc.). Then, using such a semantic as a basis, we should be able to define a compositional proof system where verification boils down to constrain satisfaction. As mentioned before, beside the theoretical interest, this approach seems promising also from a practical perspective, as many efficient constraint solvers are available today.Obj 5.1.2 We will study how to combine abstract interpretation and constraints to extract "abstract models" from concrete programs (e.g. written in Java). In this setting "constraints" play a crucial role for modelling "conditions" on the environment of "open" program (a feature typical of multithreaded programs).Obj 5.1.3 We are interested also in using directly constraint based languages such as CCP (Concurrent Constraint Programming) and CHR (Constraint Handling Rules) for the specification and verification of multithreaded systems. We are therefore interested in compositional semantics and verification methodologies for these formalisms. While for CCP several results exists, this is not the case for CHR, due to the semantic complications arising from the ``multiple heads'' nature of CHR rules. Workpackage 6: "Automatic verification" Task Bo.6.1: "Symbolic Verification of multithreaded programs" On the basis of the results of the task STBo2 we plan the following activities.Obj 6.1.1 We will study symbolic methods for the verification of the resulting abstract models (e.g. using constraint-based model checkers) and "dynamic" abstraction operators (e.g. widening and acceleration) to be applied during the abtract analysis.Obj 6.1.2 We will study which existing verification and analysis tools based on constraint solvers (e.g. for linear constraints/propositional formulas) can be applied to support the resulting methodology. In particular we aim at identifying efficient solvers for the specific class of constraints arising from the verification methodology. For example, a key issue seems to be the ability to solve constraints on finite domains by assigning different values to variables involved in a constraint. It is therefore necessary to use constraint solvers which implement efficiently the ``alldifferent'' constraint.PhasesWe intend divide our activity in the following phases:First year: Obj 1.1.1, Obj 1.1.2, Obj 1.2.1, Obj 5.1.1 and Obj 5.1.3Second year Obj 1.1.3, Obj 1.2.2, Obj 1.2.3, Obj 5.1.2, Obj 6.1.1 and Obj 6.1.2.
|
