Research program
AIDA - Abstract Interpretation Design and Applications
University Co-ordinator
Università degli Studi di UDINE -
MATEMATICA E INFORMATICA - UDINE(UD)
Research Unit Leader
Moreno FALASCHI
Description
WP1: static analysis/abstract domainsTask UD1.1 In the literature we can find lots of domains which have been developed for analysis. Generally they have been developed as a suitable balance between precision of the result and execution time. Most of these are ``ad hoc'' solutions, which have not been developed considering the typical combining/refining methods of Abstr. Interpr. [CC92,FGR96,GR95,GS97]. Even for those which do have been systematically developed, the urging need for good performance in fix-point computation has generally led to sacrifice precision. The (Abstr. Interpr. based) frameworks for debugging and verification does not need to compute fix-points but just single steps of the abstract immediate consequences operators. Thus, in developing domains to be used for these tools, we can put the emphasis more on precision than on performance. With this spirit we want to develop new domains (eventually starting from the basic ones we have in [CLMV97,CGLV03,CGL01b]) by using the systematic techniques mentioned henceforth, to gain a better precision for the diagnosis and verification tools, without sacrificing too much performance. We think that many useful domains will derive from the combination of domains used for the analysis with domains used for type-checking. These domains will help programmers to find errors (statically), without providing an excessively detailed intended semantics of their programs. Because of the parametric nature of the prototype tools already developed the new ones can be obtained simply by re-implementing only the canonical operations of the new domain.WP3: Testing and DebuggingOne of the factors which has slowed down the diffusion of declarative languages as general-purpose programming languages is the lack of adequate development tools (visual ambients, debuggers, etc). In particular, in the case of functional logic languages, the development of debugging techniques is rather complex when evaluation strategies are taken into account.Task UD3.1 A first target of this task is to provide a framework for an automatic diagnosis of functional and logic functional code, i.e. a method which, given a program (functional, logic-functional) can detect errors in the code w.r.t. a (implicit or explicit) description of the semantics of the program (given an evaluation strategy). For diagnosis we will abstract debugging, which is an approximation which uses abstract interpretation techniques and allows to recognize errors in a wide class of programs, for which the user must not provide possible error symptoms.TASK UD3.2 We want to define a method for the automatic correction of declarative programs, which would allow us to repair the errors detected in the diagnosis phase. We will use machine learning techniques for the synthesis of declarative code. The search for a correct rule during the synthesis process can be done top-down (i.e., starting from very specific rules and obtaining more and more general rulesi), or bottom-up (i.e., by refining general rules in order to get more specific ones). In general, top-down methodologies are preferable for reducing the search space. Unfortunately, top-down methodologies allow to infer corrections w.r.t. a rather narrow class of programs. Bottom-up methodologies have a better correction capacity. We intend to develop a "hybrid" methodology which combines top-down and bottom-up correction, in order to repair a larger class of declarative programs (functional, logic-functional, contraint ones) in a way effective and efficient.TASK UD3.3 Another goal of this task is to apply the general framework for debugging, which is parametric w.r.t. any property of the concrete behavior of programs which can be expressed by Abstract Interpretation. We are going to apply it to some case studies suggested by the industry world. For example we want to develop tools to formally verify that code for some embedded systems cannot produce run-time overflows or, in case the verification fails, to identify program points where a run-time check on possible overflows must be introduced.TASK UD3.4 Following the program presented in this workpackage (WP3) we will develop a prototypical implementation of a debugger and a corrector for constraint languages. We will also implement a model checker working on constraints, as described in workpackage WP5.WP4: Hybrid and real-time systemsTask UD4.1 The use of constraint languages with temporal primitives such as tcc (timed concurrent constraint) [BGM95,SJG94b,SJG95,BGM00,PV01] allows to specify in a natural way a system by the set of constraints that the system satisfies in a given instant. This programming discipline allows to model naturally problems concerned with resource coordination. These constraint temporal languages have the problem that the resulting model generally has an infinite set of states. This problem has been studied in [FPV00,FPV01] with a proposal which consists of limiting the time interval for which the verification is done. This is achieved by means of an automatic and sufficiently expressive reduction of the set of states. We want to implement a model checker which uses this technique, either as an independent tool or as a compiler from constraint temporal languages to Kripke structures, which may then be given in input to more advanced model checkers, such as Spin. We are also developing some methodologies based on abstract interpretation [CC92] for reducing the set of states for the models generated by this type of languages, and hence for verifying programs without a limitation to a time interval. The implementation of our model checker will be then extended with these technologies.Task UD4.2 As an alternative, we shall explore the possibility of exploiting formal tools for the specification and verification of complex systems based on the combination of logics/automata [FM03,FM04,FMR04]. The solutions obtained by applying methodologies, techniques, and tools based on logic and automata theory will then be systematically compared with those based on abstract interpretation. A special attention will be devoted to a relevant class of reactive systems whose components evolve according to quite different time units (this is the case, for instance, of the control systems of hydroelectric power plants) and/or whose temporal properties must be specified with respect to a finite or infinite set of different time granularities (temporally indistinguishable states of the system, exponential grow/decay phenomena, etc.) [EM04].WP5: ConstraintsIn the paradigm of concurrent constraint programming (CC) there are several languages in which a notion of time allows to model naturally hybrid as well as real-time systems.Task UD5.1 We will model reactive systems by using the language TCCP. We will then study the properties of this language and we will compare it with other paradigms. We will extend the works on verification in [FPV00,FV03] by studying new model checking algorithms which will be more efficient and able to manage complex systems (with a larger or even infinite number of states). First of all, we will define a stracture able to represent simbolically the constraints which we use in our framework, as well as the algorithms which are necessary for the construction and the manipulation of such structure. The structure will extend the DDD structure in [MLAH99], in order to represent all constraints which are allowed in tccp programs. By starting from this structure we will be able to define a symbolic model checking method which will ne implemented and which we will compare with the previous exaustive method. We expect a great improvement in the resulting performance.Task UD5.2 We want to work on the definition of a method of abstraction for sets of constraints based on abstract interpretation which will allow us to define an abstract model-checking method. This will allow to deal with systems which can have variables defined over infinite domains (which may generate an infinite set of states).WP6: automatic verificationTask UD6.1 In the literature we can find lots of proposals for the verification of Functional and Logic Languages. In [CGLV03,CGL01a,CGL01b] we have introduced verification framework (Abstract Verification framework) obtained by applying Abstr. Interpr.'s techniques to semantic based verification methodologies. Such a framework, which is parametric with respect to the (abstract) property that has to be modeled, can be used to classify verification methods for Logic Programs as well as to develop new ones. These approach to verification, being based on Abstr. Interpr. techniques which are language independent, can be generalized to other paradigms. We want to extend this framework to cope with funcional languages, contextually developing new verification tools for this paradigm. Some initial results in this direction can be found in [ACE+03] where we have obtained a prototypical framework for debugging of functional programs modeled as term rewriting systems. We think that many useful results will derive from the combination of domains used for the analysis with domains which model assertion languages (typical of traditional verification). Domains of this kind may loose completeness w.r.t. the more traditional ones, but result effective, in the sense that they can be really used inside new tools to support programming of complex applications. Since the implementation of the tools which have been already realized is parametric, it is possible to obtain the implementation of the new tools by re-implementing only the canonical operations for each new domain.Task UD6.2 As for the specification and verification frameworks based on multi-level temporal structures, we shall take into consideration some interesting logic- or automaton-based solutions proposed in the literature, including linear temporal logics over integer periodicity constraints [Dem03], linear temporal logics extended with stereo operators [MPP02], extensions of monadic first and second order theories of one/k successors [MPP99], metric and layered temporal logics [Mo96], temporalized logics [FM04]), and interval temporal logics [MSV02], as far as the logical setting is concerned, and single string automata [DLM01], single-string automata extended with counters [DMP03], ultimately periodic automata [BMP03], systolic automata [MPP99], Rabin automata over trees with labelled edges and colored nodes [MP04], and temporalized automata [FM04], with respect to the automata side. More generally, during the last years several logic- and automaton-based approaches to the specification and verification of infinite-state systems have been proposed in the literature (e.g., classes of infinite graphs where interesting model checking problems are decidable) which present many contact points with the above-mentioned formal systems. We shall investigate the potentialities of abstract interpretation through a systematic comparison with the solutions achieved by using logics/automata.
|
