Home |
Personal Info |
Research |
Papers |
Teaching |
About |
Modular Analysis of Suspension Free cc Programs (AGP'96)
[Page last updated on "gennaio 13, 2005, 15:31:42".]Enea Zaffanella
Abstract
Compositional semantics allow to reason about programs in an incremental way, thus providing the formal base for the development of modular data-flow analyses. The major drawback of these semantics is their complexity, which increases as the interactions between different program modules become more sophisticated. As a consequence, the benefits of a compositional approach can be easily overcome by the incurred computational overhead. This observation applies in particular to concurrent constraint (cc) program modules, which can interact in very complicated ways by means of their synchronization primitive (the ask guard). In this work we provide a modular abstract interpretation framework for cc programs that partially solves this problem. By assuming the whole program suspension free, we show that it is possible to compositionally compute an approximation of its run-time behavior while keeping complexity under control. To this end we translate the cc program into a clp program and analyze the latter. Correctness results are easily stated in an implicative form. The approach is truly incremental and it does not depend on the chosen program decomposition; in particular no hypotheses are needed on the suspension freeness of each single module.
Available: PDF, 300 DPI, 600 DPI, and 1200 DPI PostScript, DVI, and BibTeX entry.
enea.zaffanella@unipr.it
| Home | Personal Info | Research | Papers | Teaching | About