1997 DPhil in Computer Science Oxford University
Research Work The focus of my career has always
been research. My first publication came as an undergraduate student
in 1987, when I got a prize from the Brazilian Computer Society. In
Brazil, I pursued an MSc by Research (typically taken full time over
two to three years); it was necessary to obtain funding for a PhD.
At that level, I was already interacting with the international
community, via the publication of book chapters and workshop papers.
Before pursuing a PhD degree, I took a position in a
technological institute in Brazil: a bridge between university and
industry. I took part in technology transfer projects. These early
experiences shaped my career as a researcher on formal methods with
applicability in industry.
After the PhD in Oxford, I got a permanent Lectureship in the top
Brazilian research group in formal methods. In those five years, I
established myself as an independent researcher. In that position, I
had a significant number of research students under my supervision.
I published well in top national and international venues. In the
evaluation of the Brazilian Research Council, I had the best
possible classification for my level of experience.
In 2002, I came to Britain with the expectation of establishing a collaboration with its thriving software and safety-critical industry. In 2003, a Royal Society Industry Fellowship provided the ideal opportunity to understand and contribute to the practice of formal methods working with QinetiQ.
At York, I seek to validate theories using real-world problems.
My main scientific achievements have been on the design and
justification of sound refinement-based program development and
verification techniques. I have covered theoretical and practical
integration with industry-strength technology: concurrency,
object-orientation, and testing, for instance.
In the last decade or so, I have championed the design of Circus, a new language that integrates well established notations to support the development of distributed programs. Significantly, it can take advantage of mathematical proof to verify concurrent systems that are too large for model checking (a technique favoured in industry, but with limitations in scalability.) The work on Circus has generated more than 2,500 citations. In this programme, I have led the development and justification of refinement theories, techniques, and tools to cope with control systems. We provide support for graphical notations popular with engineers, and for main-stream programming languages, like Java, that have recently become of interest to the safety-critical industry. Our work is distinctive in that it has comprehensive coverage of practical languages, rather than idealised notations. It also supports high degrees of automation to enable usability and scalability.
I have more than 100 publications. I have been invited to give
presentations at international conferences. I have also chaired the
Programme Committee of leading conferences (including FME, ICFEM,
and ICTAC). One of them was the 2nd World Congress on Formal
Methods, the 16th in the FME series of symposia, organised by Formal
Methods Europe, and arguably the most prestigious formal methods
event. The 2nd World Congress marked 10 years since the first of
these symposia was organised as a World Congress in 1999. I have
also been a member of over 40 Programme Committees. I
Currently, I am a Professor of Software Verification at the University of York, UK, and hold a Royal Academy of Engineering Chair in Emerging Technologies.