Soundness, evidence and discipline in high-assurance software

Roderick Chapman - Protean Code Limited

This talk will reflect on the need for soundness in software verification, and (more generally) the issue of trust in automated verification tools. If a tool vendor says their tool is "Sound", should you believe them? What does this really mean in practice, and what assumptions underpin such claims? If you develop trust in a tool, what effect does this have on engineers' behaviour and engineering process? Finally, we'll consider what role soundness plays for security claims in the face of an overtly malicious environment.

Download this presentation

About Roderick Chapman

Rod 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, 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. More recently, Rod turned his attention to software process, working on merging the discipline of traditional high- integrity processes with more agile approaches such as Scrum, and the philosophy of the Lean Engineering Movement. In February 2015, Rod was appointed Honorary Visiting Professor in the Department of Computer Science at the University of York.