BEGIN:VCALENDAR
CALSCALE:GREGORIAN
PRODID:-//Apple Inc.//iOS 6.1.3//EN
VERSION:2.0
BEGIN:VTIMEZONE
TZID:Europe/Berlin
BEGIN:DAYLIGHT
DTSTART:19810329T020000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
TZNAME:CEST
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
END:DAYLIGHT
BEGIN:STANDARD
DTSTART:19961027T030000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
TZNAME:CET
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
DESCRIPTION:Formal verification of software has finally started to become viable: we ha
 ve examples of formally verified microkernels\, realistic compilers\, hyper
 visors etc. These are huge achievements and we can expect to see even more 
 impressive results in the future but the correctness proofs depend on a num
 ber of assumptions about the Trusted Computing Base that the software depen
 ds on. Two key questions to ask are: Are the specifications of the Trusted 
 Computing Base correct? And do the implementations match the specifications
 ? I will explore the philosophical challenges and practical steps you can t
 ake in answering that question for one of the major dependencies: the hardw
 are your software runs on. I will describe the combination of formal verifi
 cation and testing that ARM uses to verify the processor specification and 
 I will talk about our current challenge: getting the specification down to 
 zero bugs while the architecture continues to evolve.
DTEND;TZID=Europe/Berlin:20171227T153000
DTSTAMP:20171220T105656Z
DTSTART;TZID=Europe/Berlin:20171227T150000
LAST-MODIFIED:20171220T105651Z
LOCATION:Saal Borg
SEQUENCE:0
SUMMARY:How can you trust formally verified software? - Alastair Reid
TRANSP:OPAQUE
UID:44e7cb13-011e-4242-b26a-1edf4ac15b83@frab.cccv.de
URL;VALUE=URI:https://fahrplan.events.ccc.de/congress/2017/Fahrplan/events/8915.html
BEGIN:VALARM
ACTION:DISPLAY
DESCRIPTION:Reminder
TRIGGER:-PT1H
UID:841C3FB1-43BD-4506-896B-19BF52666E78
X-APPLE-DEFAULT-ALARM:TRUE
X-WR-ALARMUID:841C3FB1-43BD-4506-896B-19BF52666E78
END:VALARM
END:VEVENT
END:VCALENDAR
