Pisa - Dipartimento di Informatica - Research Evaluation Exercise 1999


Systematic development
of semantics,
static analysis
and verification techniques
by abstract interpretation



Proposer: Giorgio Levi

Summary

We describe our past, current and future research activities in the area of applications of abstract interpretation theory, to semantics, analysis and verification. Most of the past activity is related to logic programming. Some current activities concern functional programming too.

Participants

Giorgio Levi, Gianluca Amato, Marco Comini, Alessandra Di Pierro, Roberta Gori, Ernesto Lastres, Rene Moreno, Fausto Spoto (full time participation).

Abstract Interpretation

Abstract interpretation is a general theory for approximating the semantics of discrete dynamic systems, originally developed by Patrick and Radhia Cousot in the late 70's as a unifying framework for specifying and validating static program analyses. The abstract semantics is an approximation of the concrete one, where exact (concrete) properties are replaced by approximated properties, modeled by an abstract domain. The framework of abstract interpretation is general enough to be applicable to any semantics. It can be useful to study hierarchies of semantics and to reconstruct data-flow analysis methods and type systems. It can be used to prove the safety of an analysis algorithm. However, it can also be used to systematically derive ``optimal'' abstract semantics from the abstract domain. The systematic design aspect can be pushed forward, by using suitable abstract domain design methodologies (e.g. domain refinements), which allow us to systematically improve the precision of the domain. A number of operators have been designed to systematically improve precision, reduce complexity, and modularize analyses by refining, simplifying and decomposing domains. Abstract interpretation was originally intended as a method for automatically generate program invariants and can be very useful in program verification. For example, a sufficient condition for the partial correctness of a program w.r.t. an intended abstraction of the semantics S (abstract specification) can be obtained by proving that S is a pre-fixpoint of the (abstract) semantic evaluation function.

Abstract interpretation is language-independent. It was particularly successful (as other semantics-based techniques) in the framework of declarative (e.g. functional, logic, constraint) languages, because of their direct mathematical semantics. Results achieved for declarative languages can be meaningful also for other more practical languages.

Past activity of the group

The original background of the group is in the semantics of logic programs. The most important results were on the definition of semantics modeling various operational properties (observables) in a compositional way [2,14], to be used as the semantic basis of analysis, verification and transformation methods. Still in the semantics area, we mention the results on the semantics of concurrent constraint languages [7,8] and of their probabilistic versions [10,11]. The activities related to abstract interpretation can be summarized as follows.

Current research grants

Pending research proposals

Short term plans and expected results

A perspective on future developments

One of the most interesting challenges for researchers in the fields of programming languages semantics and formal methods is the verification of code coming from untrusted sources. The problem arises because of the continuous weakening of one of the basic assumptions in standard software development, namely that code lives in a closed world. The new technologies lead to software architectures, where programs come from potentially untrusted sources, particularly when mobile code is allowed. This increases the flexibility of software, yet raises serious problems somewhat related to correctness. The current situation in commercial systems is far from satisfactory. Most modern programming systems rely on firewalls, which impose a serious restriction on the flexibility of mobile code, by denying access to data independently of what programs really do, namely independently of their semantics. A more flexible solution requires that ``we know what programs do in order to trust them''. One promising solution to the above problem is the approach known as Proof Carrying Code (PCC). According to the PCC approach, mobile code is supplied with a formal proof that it satisfies a specification defined by the host system, which will then simply check the proof, to ensure that the code complies with its policy. One step forward is the idea of extending compilers with proof-generation capabilities (certifying compiler). In most current (experimental) implementations of the PCC idea, properties expressed in specifications are essentially type properties and certification boils down to type inference and verification. Several techniques are available to improve the specification and certification capabilities of a PCC system. These include proof systems, model checking and dataflow analysis. We believe that abstract interpretation is now scientifically mature, although not yet fully explored in the context of automatic program certification. Abstract interpretation provides both a general enough setting where different type systems, proof methods, and dataflow analysis techniques can be reconstructed and combined, and a strong enough theory to assist in the correct specification and implementation of program certification systems. On one side, abstract interpretation can be viewed as a common interface for validating code by standard program analysis, proof methods, and type-based validation methods. On the other side, it is particularly adequate to cope with highly dynamic systems. Properties which need to be proved are in fact subject to change, because of the evolution of the environment. Several systematic design techniques are available (systematic design of the abstract semantics, systematic design of domains from the property of interest) to make it easier the adaptation to new requirements. Moreover, a program certifier which is systematically derived from the concrete language semantics is more reliable and flexible. Finally, abstract interpretation based certification methods are intrinsically modular (if the collecting semantics is compositional). This is of course relevant to the issue of scalability of the techniques.

Some of our current activities are relevant to the applicability of abstract interpretation techniques to certification in a PCC approach. In particular:

As already mentioned, in the short term we plan to tackle the above problems in the case of simple declarative languages. However, we plan to move to more realistic languages, such as those actually used to implement mobile systems, once we have obtained some results.

Short CV's

GIORGIO LEVI

ALESSANDRA DI PIERRO

 $$
Background: Theory of Logic Programming (semantics of negation, infinite computations, extensions with constraints and concurrency).
 $$
Current research interests: extensions of basic programming paradigms with probability, probabilistic approaches to the semantics and the analysis of programs.
1994
Ph.D. at the University of Pisa.
1995
Post-doc at the University of Linköping.
1996-97
Senior research fellow at the City University (London).
1998
Assistant professor at the University of Pisa.

MARCO COMINI

 $$
Research interests: semantics, abstract interpretation, verification and debugging.
1989
Admitted in the Science Class at the Scuola Normale Superiore di Pisa.
1997
Ph.D. in Computer Science at the University of Pisa.
1997
Co-chairman of the International Workshop Tools and Environments for (Constraint) Logic Programming. Post-conference workshop of the International Symposium on Logic Programming, Port Jefferson, NY (USA).
1998
Guest-researcher at Institutionen för Datavetenskap, Linköping Universitet, Sweden.
1998
Research fellowship of Consiglio Nazionale delle Ricerche.
1998
Guest-researcher at Institut National de Recherche en Informatique et en Automatique, Rocquencourt-Paris, France.
1999
Van Vleck Visiting Assistant Professor at Wesleyan University, Middletown, Connecticut, USA.
1999-
Postdoctoral fellowship at Università di Pisa.

ROBERTA GORI

1995
Degree of DEA in ``Informatique, Mathematiques et Applications''. DEA's Thesis Title: A Hierarchy for General CLP(A) Programs.
1996-1999
Ph.D. Student in Mathematical Logic and Theoretical Computer Science, Dipartimento di Matematica, University of Siena (Italy).

FAUSTO SPOTO

1996-1999
Ph.D. Student in Computer Science, Dipartimento di Informatica, University of Pisa (Italy).
1998-1999
Visiting scientist at the University of Leeds (UK).

Bibliography

1
R. Barbuti, R. Giacobazzi, and G. Levi.
A General Framework for Semantics-based Bottom-up Abstract Interpretation of Logic Programs.
ACM Transactions on Programming Languages and Systems, 15(1):133-181, 1993.

2
A. Bossi, M. Gabbrielli, G. Levi, and M. Martelli.
The s-semantics approach: Theory and applications.
Journal of Logic Programming, 19-20:149-197, 1994.

3
M. Comini, G. Levi and M.C. Meo.
A Theory of Observables for Logic Programs.
Information and Computation, (to appear).

4
M. Comini, G. Levi, M.C. Meo, and G. Vitiello.
Abstract Diagnosis.
Journal of Logic Programming, 39 (1-3):43-93, 1999.

5
M. Comini, G. Levi, and G. Vitiello.
Declarative diagnosis revisited.
In J. Lloyd, editor, Proceedings of the 1995 International Symposium on Logic Programming, pages 275-287. The MIT Press, 1995.

6
M. Comini and M. C. Meo.
Compositionality properties of SLD-derivations.
Theoretical Computer Science, 211(1-2):275-309, 1999.

7
F.S. de Boer, A. Di Pierro, and C. Palamidessi.
Nondeterminism and Infinite Computations in Constraint Programming.
Theoretical Computer Science, 151(1), 1995.
Selected Papers of the Workshop on Topology and Completion in Semantics, Chartres, France, 18-20 Nov.

8
F.S. de Boer, A. Di Pierro, and C. Palamidessi.
An Algebraic Perspective of Constraint Logic Programming.
Journal of Logic and Computation, 7(1), 1997.

9
A. Di Pierro, M. Martelli, and C. Palamidessi.
Negation as Instantiation.
Information and Computation, 120(2):263-278, August 1995.

10
A. Di Pierro and H. Wiklicky.
A Banach Space Based Semantics for Probabilistic Concurrent Constraint Programming.
In Xuemin Lin, editor, Proc. 4th Australasian Theory Symposium, CATS'98, volume 20 - 3 of Australian Computer Science Communications, pages 245-259, Singapore, 1998. Springer-Verlag.

11
A. Di Pierro and H. Wiklicky.
An Operational Semantics for Probabilistic Concurrent Constraint Programming.
In Y. Choo P. Iyer and D. Schmidt, editors, Proc. ICCL'98- International Conference on Computer Languages, IEEE Computer Society and ACM SIGPLAN, pages 174-183, Chicago, 1998. IEEE Computer Society Press.

12
F. Fages and R. Gori.
A hierarchy of semantics for normal constraint logic programs.
In M. Hanus, M. Rodriguez-Artalejo, editors, Proc. Fifth Int'l Conf. on Algebraic and Logic Programming, volume 1139 of Lecture Notes in Computer Science, pages 77-91. Springer-Verlag, 1996.

13
F. Fages and R. Gori.
Analysis of normal logic programs.
In G. Levi, editor, Static Analysis, Proceedings of the Fifth International Static Analysis Symposium SAS 98, volume 1503 of Lecture Notes in Computer Science, pages 82-98. Springer-Verlag, 1998.

14
M Gabbrielli, G. Levi, and M. C. Meo.
Observable Behaviors and Equivalences of Logic Programs.
Information and Computation, 122(1):1-29, 1995.

15
R. Giacobazzi, S.K. Debray, and G. Levi.
Generalized Semantics and Abstract Interpretation for Constraint Logic Programs.
Journal of Logic Programming, 25(3):191-247, 1995.

16
R. Gori and G. Levi.
Finite failure is and-compositional.
Journal of Logic and Computation, 7(6):753-776, 1997.

17
Giorgio Levi and Fausto Spoto.
An Experiment in Domain Refinement: Type Domains and Type Representations for Logic Programs.
In Catuscia Palamidessi, Hugh Glaser, and Karl Meinke, editors, Proceedings of the 10th International Symposium on Programming Languages, Implementations, Logics and Programs, PLILP'98, volume 1490 of Lecture Notes in Computer Science, pages 152-169, Pisa, Italy, September 1998. ©Springer-Verlag.

18
Levi, G. and Volpe, P.
Derivation of Proof Methods by Abstract Interpretation.
In Catuscia Palamidessi, Hugh Glaser, and Karl Meinke, editors, Proceedings of the 10th International Symposium on Programming Languages, Implementations, Logics and Programs, PLILP'98, volume 1490 of Lecture Notes in Computer Science, pages 102-117, Pisa, Italy, September 1998.

19
Fausto Spoto.
Operational and Goal-Independent Denotational Semantics for Prolog with Cut.
Journal of Logic Programming, 1999.
To appear.

20
Fausto Spoto and Giorgio Levi.
Abstract Interpretation of Prolog Programs.
In A.M. Haeberer, editor, Proceedings of the 7th International Conference on Algebraic Methodology and Software Technology, AMAST'98, volume 1548 of Lecture Notes in Computer Science, pages 455-470, Amazonia, Manaus, Brazil, January 1999. ©Springer-Verlag.

Collaborators

Roberto Bagnara (University of Parma), Roberto Giacobazzi (University of Verona), Chris Hankin (Imperial College), Patricia Hill (University of Leeds), Jim Lipton (Wesleyan University) , Maria Chiara Meo (University of L'Aquila)

Keywords

Abstract interpretation, semantics, static analysis, verification, logic programming.



Index Page