- Carlo Ghezzi, Politecnico di Milano, I
- Benjamin Pierce, University of Pennsylvania, USA
- CC: George Necula, University of California, Berkeley, USA
- ESOP: Sophia Drossopoulou, Imperial College London, UK
- FASE: Francisco Curbera, IBM TJ Watson, USA
- FOSSACS: Wan Fokkink, Vrije Universiteit Amsterdam, NL
- TACAS: Somesh Jha, University of Wisconsin, Madison, USA
Types for Hierarchic Shapes
Invited ESOP Talk by Sophia Drossopoulou
Sophia Drossopoulou, Imperial College London, UK
Monday, March 27, 09:00 - 10:00
Abstract
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
Abstract
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
Abstract
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
Abstract
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
Abstract
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
Abstract
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
Abstract
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