Past Activities

The following are particulars about some of my main research and development activities in the past:

  • Relational databases: I have designed an experimental relational database management system for the PDP-11 mini computers. This design has much in common with the design of the well-known System R which was independently developed at about the same time for IBM main frames. I have also developed an extremely space efficient algorithm for the evaluation of database queries expressed in the relational calculus, which was, about 45 years ago, my first formal software development activity. I have specified the query evaluation problem and verified the correctness of the algorithm using classical first-order logic and elementary set theory.
  • Programming languages and compiler construction: I have been involved in the design of the programming language CHILL and the construction of a compiler for it. One of my main contributions to the compiler construction have been the detailed design of the translation phase of the compiler by means of VDM. I have devised a new approach where code generation is driven by simulation of program execution on an abstract machine. The starting-point of the rigorous design of the translation phase was the formal definition of CHILL to which I have contributed as well. The design turned out to be highly reusable when the compiler had to be adapted to new target machines.
  • Formal methods (VVSL): I have designed a specification language, called VVSL, which extends the language used in the software development method VDM with features for specifying interfering operations and modular structuring of specifications. The approach to the specification of interfering operations encompasses various other approaches. VVSL is probably the only language for writing modularly structured VDM specifications with a sound mathematical basis for its modular structuring features. I have also used VVSL to formalize the relational database model and a model of transaction management in database systems. Many formerly unmentioned assumptions in most work on databases have been made explicit in these formalizations.
  • Formal methods (SDL): I have worked on various topics aimed at achieving advances in the area of analysis of systems described using SDL, a specification language widely used in telecommunications. My work on a new semantics of a fragment of SDL, based on a process algebra with discrete relative timing, is most known. Unlike in related work, the chosen fragment covers all behavioural aspects of SDL and the proposed semantics agrees with the official semantics as far as possible.
  • Concurrency theory: I have made a systematic study of issues relevant to dealing with timing in process algebra. This work has, first of all, resulted in a coherent collection of four ACP-style process algebras, each dealing with timing in a different way. Another result of my work on process algebra with timing is a process algebra for hybrid systems which has considerably more potential with regard to description and analysis than the ones proposed earlier. My model-theoretic investigation of first-order extensions of process algebras sets an interesting new direction for future research in the field of process algebra.
  • Theory of programs: In the setting of an algebraic theory of instruction sequences, called PGA, I have investigated issues concerning the following subjects from the viewpoint that a program primarily represents an instruction sequence: programming language semantics, programming language expressiveness, computability, computational complexity, algorithm efficiency, algorithmic equivalence of programs, program performance, program compactness, program parallelization, and program verification. This work demonstrates that the notion of instruction sequence is relevant to diverse subjects from computer science.