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.
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.