Theseus
   

   DisCoTec 07

        Federated Conferences:
             Coordination 07
             DAIS 07
             FMOODS 07
        Invited speakers
        Satellite events
        Location
        Registration
        Contact us

   Related Events

        

 

 

 

 

 

 

 

 

 

 

 

DisCoTec 07

Mariangiola Dezani-Ciancaglini
Dean, Computer Science Department
University of Torino, Italy
Session Types for Object-Oriented Languages

A session takes place between two parties; after establishing a connection, each party interleaves local computations with communications (sending or receiving) with the other. Session types have been introduced to guarantee consistency of the exchanged data and, more recently, progress of the session, i.e. the property that once a communication has been established, well-typed programs will never starve at communication points. We study the incorporation of session types into object-oriented languages through a multi-threaded language with thread spawning, iterative and higher-order sessions, and bounded polymorphism. For this language we discuss synchronous versus asynchronous communication.

Mariangiola Dezani-Ciancaglini is full professor of "Foundations of Computer Science'' at the University of Torino. She introduced the intersection type assignment systems, which were largely used as finitary descriptions of lambda-models. More recently, she is interested in type systems for object-oriented languages and ambient calculi.

************************************************************************

Rachid Guerraoui
School of Computer and Communication Sciences
Ecole Polytechnique Federale de Lausanne
Sommersby: The Return of the Transaction

The transaction is back, this time in the form of a shared memory abstraction within concurrent programming languages; hence the name: shared memory transaction. This looks very much like the old database transaction. But is it the same? A jury has examined the case and is arguing that, although they are similar in spirit, the shared memory transaction has specifities that induce different challenges than those extensively addressed in he database world. There is space for interesting research in this area and this might not always be about re-inventing the wheel.

Rachid Guerraoui is professor at the School of Computer and Communication Systems at EPFL (lpdwww.epfl.ch). He graduated from Univ of Orsay and has been affiliated with Centre de Recherche of Ecole de Mines de Paris, Commissariat l'Energie Atomique in Saclay, Hewlett-Packard in Palo Alto and the Massachusets Institute of Technology. He is interested in distributed algorithms and programming languages, as well as wine and triathlons.

************************************************************************

Wolfgang Ahrendt
Chalmers University of Technology, Göteborg
Title: KeY - A Formal Method for Object-Oriented Systems (in collaboration with Bernhard Beckert, Reiner Hähnle, Peter H. Schmitt)

KeY is project and system for the formal development of object-oriented software. A major aim of KeY is the integration of formal specification and verification into standard work flows and tools for software development. For that, the core of the system, the KeY prover, is integrated into the open IDE Eclipse and the CASE tool Borland Together. Supported specification languages are UML/OCL and JML. The heart of the system is a novel interactive/automated prover for Dynamic Logic for Java source code. The KeY prover features a user-friendly graphical interface, a proof confluent sequent calculus, explicit delayed substitutions, and a simple and powerful theory formalization language called 'taclets', among other aspects.

Wolfgang Ahrendt is Senior Lecturer at Chalmers University of Technology in Göteborg, Sweden. He took his Ph.D. from the University of Karlsruhe in 2001, with a thesis on 'Deductive Search for Errors in Abstract Data Types'. His work mainly falls in the areas of Software Verification and Automated Theorem Proving. He co-authored several articles and tutorials on KeY, and wrote a book chapter on how to use KeY.


************************************************************************

Rocco De Nicola
Universita' di Firenze
Title: Quantitative analysis of Mobile and Distribute Systems: The Klaim Approach

Global (or network-aware) computing deals with the issue of programming and evaluating large-scale networks of computers performing tasks in a cooperative and coordinated manner. Klaim is a programming and modeling languages that focus on key functional aspects of global computing such as distribution awareness, code and agent mobility, and privacy aspects. After a short review of Klaim, we shall present StoKlaim, a stochastic extension of Klaim whose semantics is based on continuous-time Markov chains; the new modelling language permits describing random phenomena such as spontaneous computer crashes and spurious network hick ups. We will then show how to reason about performance and dependability aspects of mobile distributed systems modelled as StoKlaim terms by introducing the temporal logic MoSL (Mobile Stochastic Logic). MOSL is inspired by (an action-based version of) CSL and has specific operators for quantitative analysis of systems; we shall also discuss how its formulae can be model-checked against StoKlaim specifications by taking advantage of the original model checker for CSL.