• Franz Lichtenberger: Introduction to coalgebras and coinduction (part 3).
  

• Wolfgang Schreiner: Biological Systems as Concurrent Processes (Part 1)
  

• Wolfgang Schreiner: Biological Systems as Concurrent Processes (Part 2)
  

• Nikolaj Popov: Logical Aspects of Algorithm Verification

• Marcus Caba: A Tool for Discovering and Debugging Algebraic Specifications of Java Classes

• Nikolaj Popov: Using Computer Algebra Techniques for the Specification, Verification and Synthesis of Recursive Programs
  
  We describe an innovative method for proving total correctness of tail recursive programs having a specific structure, namely programs in which an auxiliary tail recursive function is driven by a main nonrecursive function, and only the specification of the main
  function is provided. The specification of the auxiliary function is obtained almost fully automatically by solving coupled linear recursive sequences with constant coefficients. The process is carried out by means of CA (Computer Algebra) and AC (Algorithmic Combinatorics). We demonstrate this method on an example involving polynomial expressions.
  
  Furthermore, we develop a method for synthesis of recursive programs for computing polynomial expressions of a fixed degree by means of "cheap" operations e.g., additions, subtractions and multiplications. For a given polynomial expression, we define its recursive program in a schemewise manner.
  
  The correctness of the synthesized programs follows from the general correctness of the synthesis method, which is proven once for all, using the verification method presented in the first part of this talk.

• Gabor Guta: Formal Models for XML.
  

• HETEROGENEOUS FINITE-SOURCE RETRIAL QUEUES
  

J. Sztrik, Full Professor

Faculty of Informatics,
University of Debrecen, Debrecen, Hungary
jsztrik@inf.unideb.hu, http://irh.inf.unideb.hu/user/jsztrik

In this talk we investigate a single server retrial queue with a finite number of heterogeneous sources of calls. It is assumed when a given source is idle it will generate a primary call after an exponentially distributed time. If the server is free at the time of the request's arrival then the call starts to be served. The service time is also exponentially distributed. During the service time the source cannot generate a new primary call. After service the source moves into free state and can generate a new call again. If the server is busy at the time of the arrival of a primary call, then the source starts generating so called repeated calls with exponentially distributed times until it finds the server free. As before, after service the source becomes free and can generate a new primary call again. We assume that the primary calls, repeated attempts and service times are mutually independent. This queueing system and its variants could be used to model magnetic disk memory systems, local area networks with CSMA/CD protocols and collision avoidance local area networks.

The novelty of this model is the heterogeneity of the calls, which means that each call is characterized by its own arrival, repeated and service rates. The aim of the investigation is to give the usual steady-state performance measures of the system. To do so, an efficient software tool, MOSEL ( Modeling, Specification and Evaluation Language ) developed at the University of Erlangen, Germany, is used to formulate and solve the problem. Several sample numerical results illustrate the power of the tool showing the effect of different parameters on the system measures.

• Gabor Guta: Tree Query and Transformation Techniques
• Nikolaj Popov: Proving Termination or How to Avoid Proving Termination
  

• Andreas Duscher: Process Definition Languages for Mathematical Services.