Seminars

  • Typing Safe Deallocation

    Gérard Boudol

    INRIA Sophia Antipolis

    Abstract: 

    In this work we address the problem of proving, by static analysis means, that allocating and deallocating regions in the store provides a safe way to achieve memory management. That is, the goal is to provably ensure that a program does not use pointers into a deallocated region. A well-known approach to this problem is the one of Tofte and Talpin. Our first contribution is to provide a simple proof, by means of a subject reduction property, of type safety for their region calculus. Our second, main contribution is that we actually do this for an extension of Tofte-Talpin's calculus,
    featuring a primitive construct for deallocating regions, similar to C's "free", that allows one to circumvent the strict stack-of-regions discipline enforced in Tofte-Talpin's calculus. Our static analysis consists in a novel type and effect system, extending the one of Tofte and Talpin, where we record deallocation effects.

    Where: 
    6.3.5
    When: 
    Wednesday, May 28 2008
    Time: 
    11:00
  • SoA, Workflows and Policies

    Stephan Reiff-Marganiec

    University of Leicester. StPowla

    Abstract: 

    In this talk we will introduce StPowla, a workflow based approach to business modelling that integrates a workflow notation to capture the core process and policies to capture the variability. The whole approach is linked to Service Oriented Computing in that the workflow tasks are executed by services.
    This work is conducted jointly with Carlo Montangero and Laura Semini at the University of Pisa and is partly supported by the EU Project Sensoria.

    Where: 
    6.3.5
    When: 
    Wednesday, April 30 2008
    Time: 
    11:00
  • Secure Implementations of Typed Channel Abstractions

    Marco Giunti

    FCUL

    Abstract: 

    The challenges hidden in the implementation of high-level process calculi into low-level environments are well understood. In this talk we present a secure implementation of a typed pi calculus, in which type capabilities are employed to realize the policies for the access to communication channels. Our implementation translates the typed capabilities of the high-level calculi into corresponding term capabilities protected by encryption keys only known to the intended receivers. As such, the implementation is effective even in the presence of open contexts for which no assumption on trust and behavior may be made. Our technique and results draw on, and extend, previous work on secure implementation of channel abstractions in a dialect of the join calculus. In particular, our translation preserves the forward secrecy of communications in calculi which support the dynamic exchange of write and/or read access rights among processes. We establish the adequacy and full abstraction of the implementation by contrasting the untyped equivalences of the low-level cryptographic calculus, with the typed equivalences of the high-level source calculus.

    Where: 
    6.3.5
    When: 
    Wednesday, April 16 2008
    Time: 
    11:00
  • Versioned Software Transactional Memory - An STM in the real world

    João Cachopo

    IST

    Abstract: 

    The need to simplify the programming task of multiprocessor machines has spurred intense research on the area of Software Transactional Memory (STM). Unlike traditional lock-based mechanisms, STMs promise to free the programmer from the burden of managing locks to ensure consistent access to shared memory in a concurrent environment. Yet, despite all the work made on STMs until now, most STM implementations are still in the realms of research labs, rather than being used to solve real world problems. In this talk, I describe a new design for an STM model that was driven by the needs of a real world large web application. This new STM model is based on a form of multi version concurrency control and it is specially suited for a large class of real world applications. I describe the model, its implementation, and the results of its usage in the Fénix web application over the last two years.

    Where: 
    6.3.5
    When: 
    Wednesday, March 26 2008
    Time: 
    11:00
  • Monitoring Java Code Using Congu

    Vasco T. Vasconcelos

    FCUL

    Abstract: 

    The main goal of the ConGu project is to develop a framework to create property-driven algebraic specifications and to allow testing Java implementations against these specifications. We present a brief overview of the framework's fundamental components - specifications, modules, refinements - and describe the ConGu tool both from the user's and from the architect's point of view. The tool allows users to test Java classes - no source code needed, just bytecode - against a module of specifications, and to discover runtime axiom violations. The tool generates intermediate classes equipped with contracts and wraps the original classes in classes that allow contract monitoring in a way that is transparent to the clients of the original classes. The tool generates JML assertions, but it could as well generate contracts in other assertion languages: the ConGu modules that generate classes for monitoring are independent from those that generate contracts. We also report on the use of the ConGu tool in the context of an undergraduate programming course at the University of Lisbon. [Joint work with Isabel Nunes, Antónia Lopes, João Abreu, Luís S. Reis]

    Where: 
    6.3.5
    When: 
    Wednesday, March 5 2008
    Time: 
    11:00
  • Domain-Oriented Reuse Interfaces

    André L. Santos

    FCUL

    Abstract: 

    The purpose of object-oriented frameworks is to enable the development of multiple applications of a certain domain, achieving high levels of reuse. Given the difficulty of learning a framework's reuse interface, framework developers may build a domain-specific language (DSL) for generating framework-based applications from domain-level descriptions. Typically, the DSL syntax is defined independently, while the mapping between DSL concepts/relationships and framework-based code is implemented in a code generator. A Domain-Oriented Reuse Interface (DORI) for an object-oriented framework is a reuse interface that enables the code of a framework-based application to have an unambiguous and straightforward mapping to instances of a DSL's concepts/relationships, which otherwise would not be possible by means of a conventional reuse interface. DORIs are able to play an important role when building DSL support. The straightforward mapping allows to have a generic code generator for all the frameworks with a DORI, and therefore, DSL support can be achieved without developing code generators. A DORI can be implemented in additional framework layer based on aspect-oriented programming.

    Where: 
    6.3.5
    When: 
    Wednesday, February 27 2008
    Time: 
    11:00
  • Dynamic Interfaces

    Vasco T. Vasconcelos

    FCUL

    Abstract: 

    We define a small class-based object-oriented language in which the availability of methods depends on an object's state: objects's interfaces are dynamic. We define a static type system in which the typing of a method specifies pre- and post-conditions for its object's state, and each class has a session type which provides a global specification of the availability of methods in each state. The state of an object may also depend on the result of a method whose return type is an enumeration. Linear typing guarantees unique ownership of objects. We prove a type safety theorem, and a theorem about consistency between a class's session type and the typings of its methods. We then consider inheritance and the associated subtyping relation on dynamic interfaces. A subtyping relation on session types, related to that found in previous literature, characterizes the relationship between method availability in a subclass and in its superclass. [Joint work with S. Gay and A. Ravara].

    Where: 
    6.3.5
    When: 
    Wednesday, January 9 2008
    Time: 
    11:00
  • Zas-An aspect oriented access control framework

    Paulo Zenida

    FCUL

    Abstract: 

    This work presents an access control framework for Java applications, named Zás, which can be reused and that applies the abstract reference monitor proposed by Anderson. This framework supports access control policies using different kinds of context information and allows them to be changed at runtime. Zás was developed in the aspect oriented programming language AspectJ and it uses Java 5 annotations.

    Where: 
    6.3.5
    When: 
    Sunday, January 6 2008
    Time: 
    11:00
  • Towards a flexibility framework for software processes

    Ricardo Martinho

    Abstract: 

    Software process models are dynamic entities that must evolve in order to cope with changes occurred in: the enacting process (due to changing requirements or unforeseen circumstances); the software development organization; the market; and in the methodologies used to produce software. Therefore, flexibility concepts should also be part of a process modeling meta-model, in order for process modelers to be able to express the "right" flexibility into process models, i.e., to express which, where and how flexible are the elements that compose a process model. In this workshop I'll talk about how SPEM-based software process models can support and express flexibility concepts, and also about some early developments regarding an implementation of those concepts.

    Where: 
    6.3.5
    When: 
    Wednesday, October 24 2007
    Time: 
    11:00
  • Distribuição de dados utilizando algoritmos epidémicos em redes ad hocsem fios (Gossip-based data distribution in mobile ad hoc networks)

    Hugo Miranda

    Abstract: 

    Redes ad hoc sem fios são redes de dados construidas sem o apoio de umainfra-estrutura de suporte e compostas exclusivamente por dispositivosmóveis. Assume-se que os dispositivos móveis têm recursos limitados(energia, memória e poder computacional) e podem mover-se livremente,entrando e saindo do raio de transmissão dos restantes com frequência.Devido à ausência de uma infra-estrutura de suporte, os serviços (e.g.encaminhamento, armazenamento de dados) têm que ser prestados pelospróprios dispositivos, muitas vezes de forma cooperativa para aumentar aresiliência a falhas. A apresentação descreve uma concretização de umserviço de replicação de dados em redes ad hoc sem fios. Serão abordadosos diversos algoritmos necessários à disseminação e recuperação de dadose apresentada uma aplicação para este serviço.

    Where: 
    6.3.5
    When: 
    Wednesday, September 26 2007
    Time: 
    11:00

Pages

Subscribe to Seminars