![]() |
University of Cambridge > Talks.cam > Computer Laboratory Wednesday Seminars > Correctness by Construction of High-Integrity Software
Correctness by Construction of High-Integrity SoftwareAdd to your list(s) Download to your calendar using vCal
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 Computer Laboratory Wednesday Seminars series. This talk is included in these lists:
Note that ex-directory lists are not shown. |
Other listsPhilosophy and Natural Philosophy in the Early Modern Period Cambridge PhD Training Programme in Chemical Biology & Molecular Medicine BSS Formal SeminarOther talksThe RAID project Zero Degrees of Empathy Consensus, what consensus? Looking at the genes behind Darwin’s abominable mystery Useful books: reading vernacular regimens in 16th-century England Preprocessing of fMRI data and computational morphometry (VBM) |