The software
safeguard
Professor Dino Distefano is a world leader in software
security, developing routines and systems to ensure
that complex programs are secure and reliable
and contain no hidden errors that could lead to
unintended consequences.
Research area
Dino Distefano is a Professor of
Software Verification at Queen Mary,
University of London and a pioneer
in the growing area of software
security. He leads both academic
and commercial research teams
developing mathematical models that
find mistakes in software – errors
that, in some applications, could be
safety-critical. In the same way that
compiler tools do checks in computer
programs for incorrect syntax,
Professor Distefano’ s tools construct a
mathematical model of what software
programs will do when they run and
identify when they might misbehave.
From a background of applying
mathematical logic to verify the
correctness of systems, Professor
Distefano has concentrated on software
verification for the past 10 years and
is credited with development of the
first separation logic program analysis
tool. The core theory behind this work
is to separate the computer code into
discrete areas and test the each area
individually rather than the entire code
76
PECM ssue 15
at once. For example, the separation
logic program analysis tool would
only check the memory used by the
program, and not the entire system,
and therefore would work much faster
than conventional proving tools. Under
the RAEng/EPSRC Research Fellowship,
he has been working on automating
verification of industrial and large-scale
software: programs of the kind that
are used where errors can have safety
and reliability implications. He and his
co-researchers founded a company,
Monoidics, to commercialise the results
of their research.
Academy support
Professor Distefano was backed by the
RAEng/EPSRC Research Fellowship
which helped him focus and achieve
the goal of automating the software
checking routines. He said, “I think
it’s one of the greatest things the UK
has that it gives support to young
engineers and scientists to enable
them to concentrate on their research
and be relieved of teaching and admin
duties. I don’t think I could have done
what I’ve done without this support.”
Key achievements
Developed Space Invader, the first
separation logic program analyser
Shortlisted for Times Higher
Education Supplement Research
Project of the Year, 2008
Winner, Roger Needham Award for
contributions to computer science,
British Computer Society 2012
Microsoft Research developed
internal software tool for
software verification based on his
work
Professor Distefano’s start-up
company, Monoidics, was acquired by
Facebook in July 2013