Abstract
Current data abstraction mechanisms are not adequate to control sharing of state in the general case involving objects in linked structures. The pervading possibility of sharing is a source of errors and an obstacle to language implementation techniques. Balloon types, which we have introduced in [2], are a general extension to programming languages. They make the ability to share state a first class property of a data type. The balloon invariant expresses a strong form of encapsulation: no state reachable (directly or transitively) by a balloon object is referenced by any external object. In this paper we describe the checking mechanism for balloon types. It relies on a non-trivial static analysis, described as an abstract interpretation. Here we focus in particular on the design of the abstract domain which allows the checking mechanism to work under realistic assumptions regarding possible object aliasing. ©1999 Published by Elsevier Science B. V.

Abstract
In the last few years, information outsourcing has been a current activity on large companies. Information as become a regular trading commodity. It is a well known fact that direct mailing companies acquire databases, or other kind of information sources, from other companies with names and addresses of potential clients. Also, enterprise managers are frequently concerned with the current status and welfare of their clients and suppliers. Commonly, they use to appeal to specialized external information providers which may, under certain conditions, provide them specific profiles about such potential commercial partners. On companies with effective means of information processing, it is very probable that such needs of information may be directly satisfied with data stored and managed in the companies' data warehouses. In this paper we propose a protocol based on economic principles that enables the automatic negotiation of information transference between data warehouse systems of different companies. The protocol was designed to be used by a community of intelligent agents responsible to ensure and support all the operational tasks related to information outsourcing among companies.

Abstract

Abstract

Abstract

Abstract
In this paper we argue that using verification in interactive systems development is more than just checking whether the specification of the system has all the required properties; and that changing the focus from a global specification into partial, property oriented, specifications can provide a number of advantages and make verification act as an aid to decision making. We also present a compiler that allows for the verification of interactor specifications to be done in SMV, as well as a simple case study where verification is used to inform a design decision.