Abstract
This paper sketches a reverse engineering discipline which combines formal and semi-formal methods. Central to the former is denotational semantics, expressed in the ISO/IEC 13817-1 standard specification language (VDM-SL). This is strengthened with algebra of programming, which is applied in "reverse order" so as to reconstruct formal specifications from legacy code. The latter include code slicing, a "shortcut" which trims down the complexity of handling the formal semantics of all program variables at the same time. A key point of the approach is its constructive style. Reverse calculations go as far as absorbing auxiliary variables, introducing mutual recursion (if applicable) and reversing semantic denotations into standard generic programming schemata such as cata/paramorphisms. The approach is illustrated for a small piece of code already studied in the code-slicing literature: Kernighan and Richtie's word count C programming "bagatelle".

Abstract
This paper is an attempt to apply the reasoning principles and calculational style underlying the so-called Bird-Meertens formalism to the design of process calculi, parametrized by a behaviour model. In particular, basically equational and pointfree proofs of process properties are given, relying on the universal characterisation of anamorphisms and therefore avoiding the explicit construction of bisimulations. The developed calculi can be directly implemented on a functional language supporting coinductive types, which provides a convenient way to prototype processes and assess alternative design decisions. ©2001 Published by Elsevier Science B.V.

Abstract
In this paper we address the problem of organized collective agency, and propose a deontic/action modal logic for that purpose. We argue that once we want to attribute obligations (permissions or other deontic notions) to a set of agents, we need to consider a new agent-that we called institutionalized agent, and specify how he interacts with the external world: how the obligations flow from the institutionalized agent to the real agents that support him, and how the actions of the latter count as actions of the former. But an agent may act in many qualities (roles), and it is essential to know in which quality an agent has acted, or intends to act, for three main reasons: to know the effects of the act, its deontic qualification, and authentication issues. Thus, we extend the "sees to it" action operator with an explicit index that states the quality (role) in which the agent has acted. We also show how to associate obligations to roles, and illustrate flow this can be used to express the desired flow of obligations.

Abstract
Emerging technologies that allow a two-way communication between companies, or among companies and their customers, are changing the rules of the market, facilitating the emergence of virtual entities that have to be supported by some kind of platform. Making it is the main objective of this work, materialized in a Mobile Agent Architecture (MAA) which supports the emerging world of the m-Commerce (mobile-Commerce): the MAgnUM architecture, The MAA's development was based on the principles of process and knowledge abstraction, compositionality, reuse, formal semantics, formal evaluation, and security.

Abstract
The efficient execution of irregular data parallel applications, on dynamically shared computing clusters, requires novel approaches to manage the runtime load distribution. Stich environments have an unpredictable dynamic behaviour both due to the application requirements and to the available system's resources. This uncertainty was the main motivation to propose and evaluate an application level scheduler, where decisions are efficiently taken with improved accurate predictions on the environment's current and near future state, based on available incomplete and aged measured data. Bayesian decision networks are used as the scheduler's decision making mechanism: its effectiveness to manage the load distribution of a parallel ray tracer is assessed and compared with alternative strategies. The evaluation results, with complex scenes on a 7 shared nodes cluster with dynamically variable workloads, show considerable performance improvements over blind strategies, and stress the benefits over a sensor based deterministic approach of identical complexity.

Abstract
In this paper we describe a transaction management system designed to face the inherent characteristics of mobile environments. Mobile clients cache subsets of the database state and allow disconnected users to perform transactions independently. Transactions are specified as mobile transactional programs that are propagated and executed in the server, thus allowing the validation of transactions based on application-specific semantics. In the proposed model (as in others previously presented in literature) the final result of a transaction is only determined when the transaction is processed in the central server. Users may be notified of the results of their transactions using system support (even when they are no longer using the same application or even the same computer). Additionally, the system implements a reservation mechanism in order to guarantee the results of transactions performed in disconnected computers. © Springer-Verlag Berlin Heidelberg 2000.