~/talk

Safety-Critical Development

on YouTube 21m
Talkat FrenchKit 2017 · 2017-09-22..09-23· [rust]

speaker

name:Clément Bourgeois
links:none on file

resources

video:https://youtu.be/xbv-Q3ddOg4
slides:none on file

summary

Claims that Ada plus SPARK prover can mathematically prove absence of runtime errors and verify pre/postconditions, with real deployments on Ariane rockets, Boeing 787, F‑22, an artificial heart pump and the Orion 6 student satellite that survived longer than peers. Shows Ada 2012 contracts, ranged integer types and restrictions to create analyzable subsets, contrasts Swift features like ARC and stronger typing, and demonstrates a verified sort where the postcondition is proved.

AI-written summary · about

chapters (5)

  1. 0:00Start
  2. 3:15How is Swift safer by design than Objective-C ?
  3. 8:48What extra safety is provided by Ada ?
  4. 13:40The SPARK language
  5. 15:23Final safety-related comparison

related talks

~/search
type to search 6,249 conferences, 138,987 speakers and 185,172 talks
~/help
cmdctrl k
search every conference, speaker and series
/
focus the filter search
h
home
c
conferences
s
speakers
e
series
t
light / dark — the status bar button does the same
?
this help
esc
close this, then clear every filter — or just the search, while you are typing in it

Ignored while you are typing. Pages without a filter rail have no search to focus.