We consider a multiprocessor operating system in which each current job is guaranteed a given proportion over time of the total processor capacity. A scheduling algorithm allocates units of processor time to appropriate jobs at each time step. We measure the goodness of such a scheduler by the maximum amount by which the cumulative processor time for any job ever falls below the “fair” proportion guaranteed in the long term.

In particular we focus our attention on very simple schedulers which impose minimal computational overheads on the operating system. For several such schedulers we obtain upper and lower bounds on their deviations from fairness. The scheduling quality which is achieved depends quite considerably on the relative processor proportions required by each job.

We will outline the proofs of some of the upper and lower bounds, both for the unrestricted problem and for restricted versions where constraints are imposed on the processor proportions. Many problems remain to be investigated and we will give the results of some exploratory simulations.

This is joint research with Micah Adler, Petra Berenbrink, Tom Friedetzky, Leslie Ann Goldberg and Paul Goldberg.

In this lecture, I will show how influential has been the work of Imre in the theory of automata, languages and semigroups. I will mainly focus on two celebrated problems, the restricted star-height problem (solved) and the decidability of the dot-depth hierarchy (still open). These two problems lead to surprising developments and are currently the topic of very active research.

I will present the prominent results of Imre on both topics, and demonstrate how these results have been the motor nerve of the research in this area for the last thirty years.

I will propose a general framework for the static analysis of programs based on Kleene algebra with tests (KAT). I will show how KAT can be used to statically verify compliance with safety policies specified by security automata. The method is sound and complete over relational interpretations. I will illustrate the method on an example involving the correctness of a device driver.