Seminars

  • Interactive Interaction Constraints

    José Proença

    KU Leuven

    Abstract: 

    Interaction constraints are an expressive formalism for describing coordination patterns, such as those underlying the coordination language Reo, that can be efficiently implemented using constraint satisfaction technologies such as SAT and SMT solvers. Existing implementations of interaction constraints interact with external components only in a very simple way: interaction occurs only between rounds of constraint satisfaction. What is missing is any means for the constraint solver to interact with the external world during constraint satisfaction.

    This paper introduces interactive interaction constraints which enable interaction during constraint satisfaction, and in turn increase the expressiveness of coordination languages based on interaction constraints by allowing a larger class of operations to be considered to occur atomically. We describe how interactive interaction constraints are implemented and detail a number of strategies for guiding constraint solvers. The benefit of interactive interaction constraints is illustrated using two examples, a hotel booking system and a system of transactions with compensations. From a general perspective, our work describes how to open up and exploit constraint solvers as the basis of a coordination engine.

    Where: 
    6.3.5
    When: 
    Wednesday, July 17 2013
    Time: 
    14:00
  • Types for security and privacy of web data

    Jovanka Pantovic

    University of Novi Sad

    Abstract: 

    We present the XdPi calculus with role-based access control and a corresponding type system. This system is suitable for modeling distributed semi-structured web documents with dynamic role-based security administration. Our calculus is an extension of XdPi calculus of Gardner and Maffeis, where a network is a parallel composition of a process and a data tree. In our calculus, roles are assigned both to processes and trees. A process can read or modify data in a well-typed tree only if that role is assigned to the process. As each location has a specified policy, we show that the policy is respected during computation. A process can enable or disable a role if it is in accordance with the location policy. We discuss the policy maintenance of well-typed networks and present obtained security properties. Another important issue for publishing data on the web is privacy. The lack of privacy mechanisms can discourage people from making their data available and linked on web of data. Our current work focuses on development of a formal model which would ensure privacy protection of a single data in RDF format.

    Where: 
    6.3.5
    When: 
    Wednesday, July 10 2013
    Time: 
    14:00
  • Typing Progress in Communication-Centred Systems

    Hugo Torres Vieira

    FCUL & LaSIGE

    Abstract: 

    We present a type system for the analysis of progress in session-based communication centred systems. Our development is carried out in a minimal setting considering classic (binary) sessions, but building on and generalising previous work on progress analysis in the context of conversation types. Our contributions aim at underpinning forthcoming works on progress for session-typed systems, so as to support richer verification procedures based on a more foundational approach. Although this work does not target expressiveness, our approach already addresses challenging scenarios which are unaccounted for elsewhere in the literature, in particular systems that interleave communications on received session channels. [Joint work with Vasco Thudichum Vasconcelos]

    Where: 
    6.3.5
    When: 
    Wednesday, May 15 2013
    Time: 
    12:00
  • Coordinating phased activities while maintaining progress

    Tiago Cogumbreiro

    FCUL

    Abstract: 

    In order to develop reliable applications for parallel machines, programming languages and systems need to provide for exible parallel programming coordination techniques. Barriers, clocks and phasers constitute promising synchronisation mechanisms, but they exhibit intricate semantics and allow writing programs that can easily deadlock. We present an operational semantics and a type system for a fork/join programming model equipped with a exible variant of phasers. Our proposal allows for a precise control over the maximum number of synchronisation steps each task can be ahead of others. A type system ensures that programs do not deadlock, even when they use multiple phasers. [Joint work with Francisco Martins and Vasco Thudichum Vasconcelos]

    Where: 
    6.3.5
    When: 
    Wednesday, April 17 2013
    Time: 
    12:00
  • Model Based GUI Testing: research challenges

    Ana Paiva

    Faculdade de Engenharia da Universidade do Porto

    Abstract: 

    Graphical User Interface (GUI) testing is the process of testing a software application with a graphical front-end to guarantee that it meets its specification. Given the myriad of possible (human-computer) interactions in such a user interface, GUI software testing is a rather expensive and cumbersome phase of the whole software development cycle.
    Model based testing (MBT) can increase the systematization and automation of the testing process. Existing research work shows MBT may be also beneficial in the context of GUI testing. However there are some challenges that it is necessary to overcome.
    This talk will present some basic concepts about model based testing, some previous research work in this area, current research work and some trends for the future. In particular it will be described a novel approach, PBGT, that aims to increase the level of abstraction of the GUI models, promote reuse, diminish the effort in the modelling construction, generate test cases from models, assess testing coverage, and execute the generated test cases over a GUI.

    Where: 
    6.3.5
    When: 
    Thursday, December 6 2012
    Time: 
    13:00
  • Communication Safe Parallel Programming with Session C

    Nicholas Ng

    Imperial College London

    Abstract: 

    I'll present Session C, a session-based programming framework for message-passing based parallel programming. The framework consists of three parts: (1) a multiparty global protocol, written in a protocol description language with support for parameterised roles, (2) a runtime library for developers to implement parallel programs based on the given endpoint protocol, and (3) a type checker to ensure conformance between the implemented programs and the protocol. The static type checker allows permutations of asynchronous communication primitives as well as supporting a dynamic number of processes to spawn not known at compile time. Typable programs in the framework is guaranteed communication-safe and deadlock-free by the underlying multiparty session types theory. [Joint work with Kohei Honda and Nobuko Yoshida]

    Where: 
    6.3.5
    When: 
    Wednesday, December 5 2012
    Time: 
    13:30
  • Single-assignment forms as a basis for program verification

    Jorge Sousa Pinto

    U Minho

    Abstract: 

    A mechanism for generating verification conditions (VCs) for the iteration-free fragment of an imperative language is fundamental in any deductive program verification system. In this talk we revisit symbolic execution, weakest preconditions, and bounded model checking as VC-generation mechanisms, and propose a uniform presentation of the corresponding sets of VCs, in terms of (logical encodings of) paths in the control-flow graph of a single-assignment form of the program under analysis. This allows us to compare the mechanisms, in particular with respect to the size of the generated formulas. We finish the talk with some preliminary ideas towards a program logic for single-assignment programs.

    Where: 
    6.3.5
    When: 
    Wednesday, October 31 2012
    Time: 
    11:30
  • PESTT - An Educational Testing Tool

    Francisco Martins

    FCUL & LaSIGE

    Abstract: 

    Our society is built upon technology. TV sets, phones, cars, planes, etc. include dozens of processors that need software to make them behave as we expect. But what happens if the living room TV set software fails? Well, we may miss, say, the UEFA Euro cup final, which for some of us could be disappointing. What about a failure in the software that runs a train or a plane? There, the consequences could be far more catastrophic, potentially with huge social and financial impacts. Software ubiquity and criticality demands for a high quality of its delivery, in which testing plays a central role in detecting and reducing software failures.

    Know how to plan, design, and execute tests are skills that software engineers need to master. In this talk we present PESTT, a tool for assists in the testing activity, ranging from planning to test coverage analysis. Along the talk we go though several use case scenarios of the testing activity and show how the tool can help both the professional test engineer and the student learning how to accomplish the task. The tool is built on top of Eclipse and, as for its current version, supports unit testing based on the control flow graph of Java methods. The talk also addresses, although in less detail, the tool internals, specially the algorithms we devise and the external tools it depends on.

    Where: 
    6.3.5
    When: 
    Wednesday, July 4 2012
    Time: 
    13:30
  • Interaction-Driven Program Comprehension

    André L. Santos

    ISCTE-IUL

    Abstract: 

    In this talk we present a set of useful mechanisms for Program Comprehension that we characterize as Interaction-Driven. This designation comes from the fact that the mechanisms use the GUI of a running application as the means to communicate developer intent with respect to source code inspection, enabling developers to efficiently navigate through the source code by demonstrating program features. We propose program instrumentation (using AOP) and IDE interconnection as the means to implement the proposed mechanisms. The mechanisms will be demonstrated, and some results regarding empirical evaluations will be presented.

    Where: 
    6.3.5
    When: 
    Wednesday, June 6 2012
    Time: 
    13:30
  • Experiments in Parallel Methods for Combinatorial Optimization

    Salvador Abreu

    U. Evora and CENTRIA

    Abstract: 

    We give an overview of our work on Propagation-based Constraint solvers and methods for Constraint-based Local Search, formulated as an effective means of using parallel processors. We discuss the constraint programming paradigm, and how it maps to these two runtime approaches. We then describe several parallel designs and characterize them in terms of raw performance but also as to how they scale on multiprocessors. The range of parallel systems encompasses conventional homogeneous multicore processors, heterogeneous multicores such as Cell/BE and clusters of such systems. We provide experimental results on large scale parallel systems, and claim that these methods are both convenient for programming solutions to a significant class of problems and effective in using large-scale parallel hardware.

    This is joint work with D. Diaz, P. Codognet, V. Pedro and R. Machado.

    Where: 
    6.3.5
    When: 
    Wednesday, May 2 2012
    Time: 
    13:30

Pages

Subscribe to Seminars