10 May 2012
Dino Distefano, lecturer at the Department of Computer Science at Queen Mary, University of London, has been named as the winner of the BCS Roger Needham Award sponsored by Microsoft Research Cambridge. Distefano’s pioneering work, which detects possible weaknesses in code, is hugely beneficial to writers who want to ensure their code is more secure from hacker’s attempts to crack it.
The Roger Needham award is sponsored by Microsoft Research Cambridge and established in memory of Microsoft’s first director of research outside the US. It is awarded for a distinguished research contribution in computer science by a UK based researcher within ten years of their PhD.
Distefano says of receiving the award: “I’m delighted and honoured to receive the BCS Needham Award. I'm very pleased with the level of progress achieved in the last few years in automatic verification and I am grateful that the work on this domain has received so much attention.”
A Royal Academy of Engineering and EPSRC Research Fellow, Distefano has led the move towards practical use of the mathematical theory called Separation Logic; a theory that addresses the problem of how computer memory stores and updates information.
Distefano has developed practical applications of this logic, by designing a new technology which makes computers more reliable. It ensures that software runs right first time by identifying and even eliminating a frequent source of errors that are caused by misuse of computer memory. Teams at the universities of Princeton, Cambridge, Berkeley, and companies such as Microsoft, are now building tools based on Distefano's ideas.
In addition, Distefano co-founded Monoidics a high-tech start-up based in the London Silicon Roundabout, developing commercial verification and analysis software products which stem from his pioneering concepts. Monoidics' products are used by customers in embedded safety critical and security-critical domains for quality assurance.
Distefano adds: “My motto and goal is ‘proofs for the masses’. I believe that one day it will be possible to bring verification technology, and with it, mathematical proofs of correct memory usage to every developer. One day programmers will use automatic verification tools as they use compilers today.”
Ken Wood, Deputy Managing Director, Microsoft Research Cambridge said: “We are delighted to be sponsoring the Roger Needham award again. Dino Distefano is a very deserving recipient of the award; his originality and vision have been a driving force in the efforts to crack the longstanding problem of tractable automatic reasoning about programs that use dynamically allocated objects, initially proposing techniques such as bi-abduction and adaptive analysis, as well as the tool Space Invader.”
Distefano will present the 2012 BCS Needham lecture on 29 November at the Royal Society, details can be found: www.bcs.org/needham/2012