Types for Hierarchic Shapes

Invited ESOP Talk by Sophia Drossopoulou

Sophia Drossopoulou, Imperial College London, UK

Monday, March 27, 09:00 - 10:00


Heap entities tend to contain complex references to each other; to manage this complexity, types which express shapes and hierarchies have been suggested. We survey type systems which describe such hierarchic shapes, and how these types are being suggested to support reasoning about programs, and program optimization.

A Programming Model for Service Oriented Applications

Invited FASE Talk by Francisco Curbera

Francisco Curbera, IBM TJ Watson, USA

Tuesday, March 28, 08:30 - 09:30


Service oriented computing (SOC) and service oriented architectures introduce a model for distributed software components. Full inter-component interoperability, based on Web services standards, is a core assumption of the SOC model. SOC, as a platform independent approach to software development and management, is not limited to a particular distributed computing stack (Web services), since the benefits of a distributed component model extend to legacy protocols and platforms as well. Web services has successfully stressed the notion that implementation characteristics should be decoupled from interoperability concerns, and has focused on defining an XML based interoperability stack. SOC is directly concerned with the implementation and management of service oriented applications and stresses the ability to incorporate multiple runtimes and programming models into an architecture of distributed software components.

The Service Component Architecture (SCA) is the first realization of SOC as an explicit component model. Just as and Web Services provide the common abstraction of interoperability concerns, SCA provides a common abstraction of implementation concerns. SCA introduces a common notion of service components, service types and service implementations as well as an assembly model for service oriented applications. SCA's goal is to be able to accommodate multiple implementation platforms into a single set of component oriented abstractions. J2EE, BPEL4WS, COBOL, SQL or XML components are only part of the possible implementation artifacts that SCA intends to support. Portability of component assemblies and implementations is an important concern of SCA.

Because it provides a venue for realizing the SOC model in practice, and given its wide support in the industry, the impact of SCA on the software industry is likely to be very large. SCA is already is backed by a Java open source initiative in Apache.

An initiative so ambitious necessarily raises many open issues. Foremost among them is the formalization of an SCA runtime model sufficiently complete to ensure portability of implementations, but at the same time generic enough that it can be supported by multiple platforms and programming models. Once an SCA runtime model is defined, the question arises of whether a native SCA platform would be able to provide better support for the execution and deployment of SOC applications. Other significant issues include the possibility of formalizing the component and assembly models beyond their current state, and the support for non-functional requirements and capabilities in the definition and assembly of components.

This talk will review the motivation and major elements of the SCA model, and will discuss the main of the open issues surrounding the SCA effort.

Software Engineering: Emerging Goals and Lasting Problems

Unifying Invited Talk by Carlo Ghezzi

Carlo Ghezzi, Politecnico di Milano, I

Wednesday, March 29, 08:30 - 09:30


Software has been evolving from pre-defined, monolithic, centralized architectures to increasingly decentralized, distributed, dynamically composed federations of components. Software processes have been evolving along similar lines, from pre-specified sequential work- flows to decentralized and multi-organization endeavors. The organizations to which software solutions are targeted have also been evolving from highly structured corporates to agile and networked enterprises. All this is affecting the way software is engineered (i.e., conceived, architected, and produced). New difficult challenges arise, while old fundamental problems are still with us. The talk surveys this evolution and tries to identify achievements, challenges, and research directions.

The Weird World of Bi-Directional Programming

Unifying Invited Talk by Benjamin Pierce

Benjamin Pierce, University of Pennsylvania, USA

Wednesday, March 29, 14:00 - 15:00


Programs generally work in just one direction, from input to answer. But sometimes we need a program to work in two directions: after calculating an answer, we want to update the answer and then somehow calculate backwards to find a correspondingly updated input. Of course, in general, a given update to the answer may not correspond to a unique update on the input, or to any at all; we need an update translation policy that tells us which updates can be translated and how to choose among translations when there are many possibilities. The question of how to determine such a policy has been called the view update problem in the database literature.

Many approaches to this problem have been devised over the years; most have taken existing database query languages (such as SQL) as their starting points and then proposed ways of describing or inferring update policies. More recently, several groups have begun working to design entirely new languages in which programs are inherently bi-directional - i.e., in which every program can be read from left to right as a map from inputs to answers and from right to left as (roughly) a map from updated answers to updated inputs. Moreover, bi-directionality in these languages is treated compositionally: each primitive works in both directions, and the two directions of compound programs can be derived from the two directions of their subcomponents.

This talk charts some interesting regions of the world of bidirectional programming and bi-directional language design, using as a touchstone our experiences at the University of Pennsylvania in the context of the Harmony project, where bi-directional languages - one for transforming trees and another for relational data - play a crucial role in the architecture of a universal data synchronizer.

Distributed Model-Checking Algorithms for WPDS with Applications to Trust-Management Systems

Invited TACAS Talk by Somesh Jha

Somesh Jha, University of Wisconsin, Madison, USA

Thursday, March 30, 08:30 - 09:30


Formal-method techniques have been applied to a variety of problems in information security. I will talk about my favorite examples and then focus on a specific example, i.e., applications of model-checking algorithms for pushdown systems to authorization problems in trust-management systems. The authorization problem is to decide whether, according to a security policy, some principal should be allowed access to a resource. In the trust-management system SPKI/SDSI, the security policy is given by a set of certificates, and proofs of authorization take the form of certificate chains. The certificate-chain-discovery problem is to discover a proof of authorization for a given request. Certificate-chain-discovery algorithms for SPKI/SDSI have been investigated by several researchers. We consider a variant of the certificate-chain discovery problem where the certificates are distributed over a number of servers, which then have to cooperate to identify the proof of authorization for a given request. We propose two protocols for this purpose. These protocols can also handle cases where certificates are labeled with weights and where multiple certificate chains must be combined to form a proof of authorization. We have implemented these protocols in a prototype and report preliminary results of our evaluation.

Oh Mega Completeness

Invited FOSSACS Talk by Wan Fokkink

Wan Fokkink, Vrije Universiteit Amsterdam, NL

Thursday, March 30, 14:00 - 15:00


In his CONCUR'90 paper, Rob van Glabbeek introduced sound and ground-complete axiomatizations for the basic process algebra BCCSP, modulo the semantics in his linear time - branching time spectrum. Also at CONCUR'90, Jan Friso Groote was the first to address whether these axiomatizations are omega-complete.

Since then, positive and negative results have been obtained regarding the existence of omega-complete axiomatizations for BCCSP modulo the semantics in the aforementioned spectrum. In this talk I will give an overview of these results, the methods that were used to obtain them, and the remaining open questions.

Using Dependent Types to Port Type Systems to Low-Level Languages

Invited CC Talk by George Necula

George Necula, University of California, Berkeley, USA

Friday, March 31, 08:30 - 09:30


A major difficulty when trying to apply high-level type systems to low-level languages is that we must reason about relationships between values. For example, in a low-level implementation of object-oriented dynamic dispatch we must ensure that the self argument passed to the method is the same object from whose virtual table we fetched the pointer to the method. Similarly, in low-level code using arrays we must relate the array address with the variables that store the bounds. We show for several examples that the high-level type system must be extended with dependent types in order to reason about low-level code. The novel feature in this use of dependent types is that they can be used in presence of pointers and mutation. We discuss three case studies. First, we show a variant of bytecode verification that operates on the assembly language output of a native code compiler. Second, we show how to express and check at the assembly level the invariants enforced by CCured, a source-level instrumentation tool that guarantees type safety in legacy C programs. Finally, we show that dependent types are a natural specification mechanism for enforcing common safe programming practices in C programs. We have used this mechanism to efficiently enforce memory safety for several Linux device drivers.
ETAPS 2006 | Top | HTML 4.01 | Last Update: 2006-02-15