Verification of Trustworthy Software

Verification of Trustworthy Software is key to preserving reliability of integrated digital systems, minimising problems caused by software errors. Unlike verification standards and methods that have been developed for more traditional industrial products, commercial software verification is often lacking. To a large degree, this is due to the inherent complexity, less controllability, and far-reaching expectations often put into software that are not yet matched by generally accepted certification methods, algorithms, or software tools for automatic analysis, verification, and design of computer software. Improved methods for creating trustworthy software can have important economic benefits by enabling companies to avoid software malfunctions. Furthermore, software developers gain competitive advantages when they can certify certain quality attributes of their products.

Strategic Priorities:

• Make use of Program Analysis Techniques to improve Software Development.
• Develop a theory of composable cyber-security protocols to offer visual accounts of organisational cyber-security protocols understandable to non-experts.
• Identify practically motivated challenges for basic research not yet covered by existing methodologies.

Pilot Research

• Development of theory and tool support for cyber-security protocols.
• Emerging problems in formal methods.