[Chiara]

Program Analysis & Logic Programming

Analyzing the Natural Semantics of Programs


We are working with our colleagues Roberto Bagnara and Enea Zaffanella in Parma on the development of CLAIR: The Combined Language and Abstract Interpretation Resource. The CLAIR system has been developed in order to study and experiment with various aspects of programming language implementation. At present, CLAIR supports two languages: a simple functional language (SFL) and an imperative language (SIL) that recalls Pascal to some extent. There is also, under development an interface to the C language via CIL - Infrastructure for C Program Analysis and Transformation [NecMR02].

The underlying approach is to base the formal semantics of CLAIR on Structured Operational Semantics [Plo81] while doing the implementation in Prolog. One of the advantages of this combination is that there is a close link between the formal specification and the implementation making it relatively easy to extend the system so as to support other language features. In addition, one can see, with relatively little effort, theory at work: a grammar becomes a parser, static semantics rules directly translate into a type checker, and with dynamic semantics rules you have an interpreter for your language.

It is planned to use CLAIR with the PPL (which already has an interface for Prolog) so as to support research into the static analysis of C programs for numerical information.


[Plo81] Gordon Plotkin. A structural approach to operational semantics. Technical Report DAIMI FN-19, Computer Science Department, University of Aarhus, Denmark, 1981.
[NecMR02] G.C. Necula, S. McPeak, S.P. Rahul and W. Weimer, CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs, in Computational Complexity, pages 213-228, 2002 Lecture Notes in Computer Science, 2304, Springer, 2002.