Celebrating Associate Professor Lindsay Groves
Associate Professor Lindsay Groves, from the School of Engineering and Computer Science (ECS), who has been instrumental in designing some of the School’s core engineering courses, retires after more than 30 years at Victoria University of Wellington.
A degree in music is what he initially wanted to pursue. Instead, Lindsay opted for a degree in pure and applied mathematics at the University of Auckland. As part of a numerical analysis course, he got into computing in his second and third years and realised how much he enjoyed solving problems and logical puzzles. Little wonder then that an advertisement for a Masters’ programme in Computer Science at Massey caught his interest. “I figured that if I could get credit for all the time I spent writing programs instead of it detracting from my coursework, why not?” he says. “There’s something special about actually writing a program, as compared to using one to solve a problem.”
After completing his Master’s degree at Massey, Lindsay moved to Wellington and started working with the Applied Mathematics Division of what was then the Department of Scientific and Industrial Research. “It was at this time, back in the 70s, that I met people who were in the maths department then, Rob Goldblatt, Megan Clark and many others. Two years later, I went back to Massey as a junior lecturer.”
Lindsay moved to teach at Waikato University in 1980, before starting his journey with Victoria University of Wellington in 1985. His research interest lies in formal methods for software specification and design. “Essentially, the field is program verification. I started out interested in a wide range of things but realised it was programming languages, programming methodology in artificial intelligence and theorem proving and program verification that I was keen on. I was also very interested in program synthesis for a long time, and in fact, that’s something I’d like to go back to at some point.”
Program verification is about using techniques from mathematical logic to establish correctness of computer programs, to ensure that the program does what we want it to. A large part it is being able to precisely identify what you want it to do, which is where the specification aspect comes in. “The field has evolved over the years though most of the foundations have stayed the same – Floyd’s work and Hoare logic are still extremely relevant to everything that we do. The biggest change is probably that computers have become bigger and faster, and it’s been far more important to build practical tools.”
Another change that Lindsay has observed is large companies getting serious about program verification. “The fact that companies like Facebook, Twitter and Amazon are employing top researchers to work on the verification and security of their systems signals a big change in the way things are going.”
Currently, Lindsay is the course coordinator for Software Correctness, or what is commonly referred to as SWEN324. “I think the course adds a lot of value to students because it introduces them to a number of key concepts – I’ve always believed that it was important to introduce students to some reasonably solid theoretical material fairly early in the curriculum. I’ve enjoyed being involved with the course and in a sense, one of the regrets that I have about leaving at this point is that I’ve taught SWEN324 in its current form only once. I’ve put in a lot of work over the years into developing the course as it evolved from being SWEN202 and SWEN224 to what it is now. It would have been exciting to take it a little further.”
Some of Lindsay’s biggest inspirations are leading names in the field. “One formative experience was going to summer school in Australia, where Sir Tony Hoare, Edsger Dijkstra and David Gries lectured us from 9 am to 6 pm for two whole weeks. I had tried to read several of Dijkstra's papers and his book and found them very heavy. But hearing Dijkstra speak in person, it just came alive for me in a way that his writing hadn't. After that experience of listening to him, I could then go and read his book, and I could actually hear him speaking, I could hear the intonation of his voice.
“And then I became interested in weakest-preconditions and predicate transformers, which has been a major part of the work that I've done in verification and refinement. When I encountered refinement calculus, it was the next big thing for me. I can't remember the first paper that I read - it was either by Carroll Morgan or Joe Morris - but I remember thinking wow! This is the next big step in the world of program verification. We had Hoare logic, we had weakest preconditions, and refinement calculus was a big step from there in presenting a constructive approach to building correct programs. It related to what was a major part of Dijkstra’s agenda - that it wasn't just about verifying programs but about constructing programs so that you know they're correct.”
Dr Stuart Marshall, Head of School, has had the opportunity to know Lindsay both as a student and a staff member. “Lindsay has been an institution at Victoria University of Wellington since I started as a student in 1993. I’ve been lucky to benefit from Lindsay’s clear-eyed analysis of key issues of the day, whether as a fresh-faced second-year student struggling to get a handle on computer science, or in the many staff meetings where Lindsay has brought a detailed analytical perspective to conversations that otherwise struggled for clarity,” he says. “He was the internal examiner for my PhD thesis back in the mid-2000s, and while at the time I was extremely nervous about getting feedback from a highly respected member of the School, the feedback I received was some of the most detailed and perceptive that I ever received. Lindsay’s presence and mana in the School will be missed.”
Also speaking about his experience of working with Lindsay, Associate Professor David Pearce says “It's been awesome working with Lindsay over the years. Not long after I arrived here, he helped open my eyes to what program verification is really about and got me interested in it. He has also been one of the last bastions ensuring students get a strong enough foundation in logic to carry them forward. It will be a struggle finding someone to carry the torch once he's gone!"
Looking back at some of his key contributions to the field, Lindsay knows that the work he did with Ray Nickson on tool support for refinement calculus actually was well ahead of its time. “Beyond that, I think the work we did with non-blocking algorithms was significant. We did the first mechanical mechanised proofs of correctness of non-blocking algorithms and essentially laid down the basic methodology that is still being used by a lot of people for doing proofs in those areas.”
Over the course of his career, Lindsay has collaborated extensively with researchers from the University of Waikato and the University of Auckland in New Zealand, the University of Queensland in Australia, and the University of Sheffield, Oxford University and the University of Surrey in the United Kingdom. He has also collaborated with organisations like Sun Microsystems and Oracle.
“Retirement after such a long career is definitely a strange prospect, especially since it came up when I was on study leave. I’m certainly not intending to put away everything that I’m doing, I will continue with some of my research collaborations for the time-being. But I do have other things that I need to work on, at home. And it’s certainly an opportunity for me to focus on other things that I like.”