RICERCA ITALIANA     

AIDA2007 - Abstract Interpretation Design and Applications

Università degli Studi di Padova

Abstract

Information sciences and technologies face the great challenge of developing effective methodologies, technologies, and tools for the requirement specification, architecture design, implementation, verification and test, deployment, maintenance and protection in workings and evolutions of composable, reliable, flexible, scalable and robust software. Scientific breakthroughs and innovation are required to maintain and gain market shares. Abstraction, as formalized by abstract interpretation, is mandatory in the development, integration, verification, analysis, testing and protection processes. The aim of the AIDA2007 project -- which is the continuation of the past successful AIDA2004 project -- is to strengthen the Italian research in abstract interpretation, by promoting abstract interpretation as a basic enabling technology required to build dependable software systems. Abstract interpretation will serve as the foundational theory to design methodologies and to build tools to ensure the interoperability, composability, scalability, reliability, robustness, dependability, security and autonomous self-adaptation of software. This theory has been proved to be a key technology for sequential, constraint, parallel (synchronous or asynchronous), distributed and mobile software as found in software and services -- whether centralized, distributed or embedded -- and has been recently shown to scale up for large industrial applications. AIDA2007 will focus on >>>

Principal Investigator

Francesco Ranzato Università degli Studi di PADOVA

Research Objectives

The outstanding progress of software and hardware technology is at the origin of the modern information and communication society. On the one hand these technologies have provided one of the greatest economical and cultural revolution in the last century, on the other hand they represent the Achille heel of our modern society, becuase software and hardware reliability, trustworthiness, safety and security are often hard to prove. A consequence of this hazard is the increasing importance and cost of software and hardware validation. However, traditional validation methods do not scale up easily, have increasing costs, are slow and so extend time to market and do not guarantee optimal quality.

Abstract interpretation is a general theory and practice for the semantic approximation of dynamic system's behaviour. A profound unity of all well known software validation methods such as static program analysis, (abstract) model checking, type and effect systems is clearly exhibited by their formalization in terms of abstract interpretation. They all aim at obtaining safe but approximate information about the behaviour of a computer system by systematically abstracting the semantics of its specification, model or program. Abstract interpretation not only formalizes these various abstractions but also provides guidelines for their refinement and combination, and it is also the base technology for the design of tools for verification of such properties at >>>

First Results

The overall goal of the AIDA2007 project proposal is to advance the state-of-the-art of research on abstract interpretation, both on foundational and applicative levels. This will be carried out by investigating some specific tasks within the four WPs that constitute AIDA2007. The following description provides a summary of the expected results for each single task.

WP1: Abstract Interpretation Design

- Task PD-1.1: Abstract domains for model checking
Disjunctive abstract domains turn out to be particularly useful in abstract model checking, e.g. in predicate abstraction [MFHRS06] and in algorithms for computing behavioural equivalences [RT07b]. We plan to investigate how disjunctive abstract domains can be useful in abstraction refinement algorithms. Since disjunctive abstract domains can be characterized as abstract domains that are complete for set unions, we also expect to characterize classes of complete abstract domains that can be advantageously used in abstract model checking, e.g. abstract domains that are complete for some temporal operator.

- Task PR-1.1: Abstract domains for points-to and aliasing analysis of C and Java programs
The approach put forward in [EGH94] for stack pointer analysis of C programs allows for the definition of a flow- and context-sensitive analysis that is able to capture both possible and definite aliasing. The specification in [EGH94] is rather informal and >>>

Timescale

24 months

National and international background

Abstract interpretation is well known as a general and unifying theory for approximating the formal semantics of computational systems. Invented by Cousot and Cousot [CC77, CC79] in the late 1970s as a unifying framework for designing and validating static program analyses, abstract interpretation has increasingly gained popularity as a general methodology for describing and formalizing approximate computations in such diverse areas of computer science as static program analysis, program transformation, system and program verification by model checking, type systems, analysis of mobile and distributed systems, security, constraint solving, etc. As a remarkable recent example of application of abstract interpretation, ASTRÉE (http://www.astree.ens.fr/) is a static program analyzer firmly based on abstract interpretation theory that was able to prove the absence of any run-time errors in the primary flight control software of the Airbus A340 fly-by-wire system (132,000 lines of rather special C code). We are approaching the point where static analyzers based on abstract interpretation can be included in the development environments of mainstream imperative programs.

The objectives of the project AIDA2007 are structured as four WorkPackages (WPs) that have a focus on specific issues of designing and applying abstract interpretation.

WP1: Abstract Interpretation Design
WP2: Static Analysis by Abstract Interpretation
WP3 >>>