Correctness by Construction of High-Integrity Software

Add to your list(s) Download to your calendar using vCal

• Rod Chapman, Praxis High Integrity Systems
• Wednesday 11 March 2009, 14:15-15:15
• Lecture Theatre 1, Computer Laboratory.

If you have a question about this talk, please contact Mateja Jamnik.

This talk will focus Praxis’ experience in building so-called “High-Integrity” software, where ultra-low defect rate at first deployment is required for reasons of safety or security. The talk will describe Correctness by Construction (CbyC) – an engineering approach developed by Praxis for such systems, and SPARK - a programming language that is designed for strong and entirely static verification. Productivity and defect rate data from several industrial-scale CbyC projects will be presented.

Speaker’s biography:

Roderick Chapman received MEng and DPhil degrees from the University of York, England in 1991 and 1995 respectively. He is currently a principal engineer at Praxis High Integrity Systems, leading the design and development of the SPARK language and toolset. Before joining SPARK team, Rod was involved in the implementation high-integrity real-time and embedded systems, including SHOLIS (the first system implemented to the Def Stan 00-55 SIL4 standard), the Lockheed Martin C130J Mission Computer, and the MULTOS CA . Rod has presented tutorials, papers and panel sessions at many conferences, including NSA HCSS , Ada Europe, and SSTC . He is also an SEI -certified PSP instructor and a Fellow of the British Computer Society.

This talk is part of the Wednesday Seminars - Department of Computer Science and Technology series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Chris Davis' list
• Department of Computer Science and Technology talks and seminars
• Graduate-Seminars
• Guy Emerson's list
• Interested Talks
• Lecture Theatre 1, Computer Laboratory
• School of Technology
• Trust & Technology Initiative - interesting events
• Wednesday Seminars - Department of Computer Science and Technology
• bld31
• computer science
• se393's list

Note that ex-directory lists are not shown.