seminar topics available

Vladimir Mencl mencl at
Wed Nov 10 12:08:03 CET 2004


v priloze posilam seznam temat na seminar.

Vyberte si prosim a dejte mi vedet emailem. Zaalokovana temata jsou
zatim pouze
   Comega (Pavel Jezek),
   IBM Autonomic Computing (Jan Kofron) a
   CIAO (Component-Integrated ACE ORB) (Luba Bulej nebo jeho diplomant)

Seznam temat jsem taktez vyvesil na

Je potreba pokryt seminari leden. Vetsina clenu skupiny jiz mela dva
referaty na podzim, na kazdeho ale vychazi jeste jeden referat na leden.

Dejte mi prosim do konce listopadu vedet, jake tema jste si vybrali.

-------------- next part --------------
Object Systems Group (OSG) Geneve
 => ESOA: The Engineering Self-Organising Applications project (ESOA),
      funded by FNRS grant (21-68026.02), aims at enabling two or more
      programs, which do not know each other, to discover each other
      capabilities by exchanging formal specifications and proofs.
 => Self-Organising Applications: A Survey  ... & others

Agent Communication Languages (do an introductory overview)

FIPA is a non-profit organisation aimed at producing standards for the
interoperation of heterogeneous software agents.
... Foundation for Intelligent Physical Agents.

  Join Calculus - 
 experimental language based on the homonymous process calculus.  The
join-calculus programming model features concurrent processes running on
several machines, static type-checking, global lexical scope,
transparent remote communication, agent-based mobility, and some

M-Calculus - a higher-order version of the Distributed Join calculus with
programmable localities.
Alan Schmitt, Jean-Bernard Stefani: The m-calculus: a higher-order distributed
process calculus 

Acute Language (Inria)
Acute: high-level programming language design for distributed

CIAO - Component-Integrated ACE ORB

TACS 2001, LNCS 2215
Caires, L., Cardelli, L.: A Spatial Logic for Concurrency (Part I)

      We present a logic that can express properties of freshness,
      secrecy, structure, and behavior of concurrent systems. In
      addition to standard logical and temporal operators, our logic
      includes spatial operations corresponding to composition,
      local name restriction, and a primitive fresh name quantifier.
      Properties can also be defined by recursion; a central theme of
      this paper is then the combination of a logical notion of freshness
      with inductive and coinductive definitions of properties.

FASE04 LNCS 2984
Roman, G.-C., Julien, C., Payton, J.
A Formal Treatment of Context-Awareness

FOSSACS 2003, LNCS 2620
Matthew Hennessy, Massimo Merro, Julian Rathke
Towards a Behavioural Theory of Access and Mobility Control in
Distributed Systems
(Extended Abstract)

WADT 2002, LNCS2755
P. Hoffman, Verifying Generative Casl Architectural Specifications

We present a proof-calculus for architectural specifications, complete w.r.t.
their generative semantics. Architectural specifications, introduced in the
Casl specification language, are a formal mechanism for expressing
implementation steps in program development. They state that to implement a
needed unit, one may implement some other units and then assemble them in the
prescribed manner; thus they capture modular design steps in the development
process. We focus on developing verification techniques applicable to full
Casl architectural specifications, which involves, inter alia, getting around
the lack of amalgamation in the Casl institution.

  - A control flow extension for asynchronous wide-area concurrency
(formerly known as Polyphonic C#):
  - A data type extension for XML and table manipulation (formerly known
as Xen and as X#):

Peter Lee: Proof-Carrying Code

IBM Autonomic Computing - Creating self-managing computing systems

More information about the Seminar mailing list