Daniel Jackson

My work focuses on fully automatic analyses of specifications and code. The approach taken by my group attempts to be at the same time principled and pragmatic. The models underlying our analyses are simple and well-understood mathematical models (such as the relational algebra and the typed lambda calculus), which allows to build powerful and predictable analysis engines. On the other hand, our tools and notations are motivated by practical case studies. Languages and analyses interest us only to the extent that they solve important industrial problems.

My research in analysis tools has been driven recently by two questions.

• In the realm of code, we have been interested in analysing large programs to provide information for developers. What kind of analysis scales; gives accurate, predictable results; handles complicated language features smoothly; and yet exploits detailed semantic information?
• In the realm of designs and specifications, we have focused on language as well as analysis issues: what kind of notation can express fundamental decisions about the behaviour and structure of a system, and how may it be analyzed economically?