Project summary

This project is implementing an information-flow security analysis logic (previously developed by DSTG) on top of the Boogie intermediate language for software verification. This will increase the automation of the approach, and integrate support for the generation of annotations. The analysis technique has been designed by DSTG to provide higher assurance than is available through existing analysis tools. The focus on automation in this project will ensure the tool can be incorporated into current software development processes with minimal cost and effort.


View publications

Partner organization(s)


Project members

Lead investigator:

Associate Professor Mark Utting

Associate Professor in Software Eng
School of Electrical Engineering and Computer Science

Other investigator(s):

Dr Kirsten Winter

Honorary Senior Fellow
School of Electrical Engineering and Computer Science