- Automatic Program Optimisation: Partial Evaluation, Partial Deduction, and Program Transformation in general
- Automatic Program Analysis: Abstract Interpretation
- Logic Programming and Functional Programming
- Distributed Systems: Petri nets, Process Algebras
- Software Verification, Model Checking, and Program Inversion
- Reasoning about action and change: Fluent calculus
- Meta-Programming: Representation Issues
- Integrity Checking in (Deductive) Databases

In particular, I have worked on **automatic control** of program specialisation
(see, e.g., papers in
ACM Toplas
or
LOPSTR'96)
and applied partial evaluation to **deductive databases**
(J. Logic Programming).
I have also pursued the **offline cogen-approach** to specialise
Prolog programs (Dagstuhl'96,
ESOP'98,
TechRep.99)
and extended existing specialisation techniques to handle
*constraints* (New Gen.
Comp.)
or accomodate more powerful transformations such as **tupling**
and **deforestation** while keeping the fully automatic control
(JICSLP'96,
LOPSTR'96,
JLP'99).
Recently, I have been particularly interested in **combining
program specialisation and abstract interpretation**
(JICSLP'98,
PLILP'96),
studying the mathematical properties of the
**homeomorphic embedding relation**
(SAS'98 & LOPSTR'98),
as well as adapting program transformation for
**tabled logic programming**
(LOPSTR'97,
LOPSTR'97).
I have also been very much interested in
**model checking** of **infinite
state (distributed) systems**.
In particular, I believe that existing techniques for
program specialisation and abstract interpretation can be used to
automatically control the abstraction required for infinite state model
checking (PSI'99,
LOPSTR'99,
CL'2000,
PPDP'2000;
I also gave a talk at a
Schloß Ringberg seminar on this topic,
see also anothertalk
I gave at TUM, and I gave lectures for a
course
at DIKU).
I am currently developing the ProB
model checker for the B-method, using a logic programming approach.

Michael Leuschel / University of Southampton / mal@ecs.soton.ac.uk