Computer Aided Formal Reasoning

• Semi-automatic verification methods for distributed algorithms (abstract model checking)
• Logics for object oriented programming languages

Complexity Theory

• Resource free characterisations of complexity classes
• Characterisation of parallel complexity classes
• Applications to memory management problems

Type Theory and Lambda Calculi

• Programming with infinite data structures (streams, real numbers, continuations, infinite branched trees)
• Higher order syntax

Verification

• muSABRE - SAT-Based Verification of Regular Properties

Combinatorial Optimization

• Time planning
• Dynamic memory allocation

 Current Projects