Industrial Applications of Static Verification

This talk will summarize about two decades of trying to build and deploy strong static verification technology for high-integrity software. This effort has included the design of both programming languages and tools, and their application to several large real-world critical projects. We’ll start with the idealized goals for static verification and why these are so hard to achieve in practice, before moving on to cover why programming language design itself matters so much, concentrating on the SPARK language and toolset. To close, I’ll give brief tour of some of the notable projects using this technology today.

Roderick Chapman is an independent consultant software engineer. He specializes in the development of safety and security-critical systems, from requirements engineering, through architectural design and implementation, to verification, audit and assessment. Following graduation from the University of York, Rod joined Praxis (now Altran UK), and contributed to many of the company’s keynote projects, rising to the role of principal engineer for software process and design. He also led the programming language and verification research group at Praxis, leading the technical development, training, sales and marketing of the SPARK product line. Rod is a regular speaker at international conferences, and is widely recognized as a leading authority on high-integrity software development, programming language design, and software verification tools. In 2006, he was invited to become a Fellow of the British Computer Society. In 2011, Rod was the joint recipient of the inaugural Microsoft Research Verified Software Milestone Award for his contribution to the Tokeneer project. In February 2015, Rod was appointed Honorary Visiting Professor in the Department of Computer Science at the University of York.