Project summary

The DSTG Program Analysis Cell investigates the use of formal methods and program analysis for detecting software security vulnerabilities. The aim is to develop advanced tools and techniques for the simultaneous development of cyber-secure systems and the associated assurance evidence necessary to prove the systems’ lack of vulnerabilities and flaws, and resistance to attacks. The emphasis of the research is on general techniques, rather than specific solutions, allowing for a diversity of solutions and innovation to be supported. This will lead to cybersecurity principles that will endure as systems and attacks evolve into the future.

Areas of research include:

Formal security foundations - developing a formal understanding of the effects of multicore hardware, operating systems, and compilation processes on information security.

Advanced program analysis - developing automated techniques for finding security vulnerabilities during software development and evolution.

Secure software development - establishing a tool/language ecosystem supporting vulnerability analysis of software at the source code, binary and intermediate levels.


View publications

Partner organization(s)


Project members

Lead investigator:

Associate Professor Graeme Smith

Associate Professor
School of Electrical Engineering and Computer Science

Other investigator(s):

Dr Kirsten Winter

Honorary Senior Fellow
School of Electrical Engineering and Computer Science

Dr Robert Colvin

Honorary Senior Fellow & Honorary Senior Fellow
School of Electrical Engineering and Computer Science

Mr Nicholas Coughlin

PhD Candidate