BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//HiPEDS – EPSRC Centre for Doctoral Training - ECPv6.15.11//NONSGML v1.0//EN
CALSCALE:GREGORIAN
METHOD:PUBLISH
X-ORIGINAL-URL:https://wp.doc.ic.ac.uk/hipeds
X-WR-CALDESC:Events for HiPEDS – EPSRC Centre for Doctoral Training
REFRESH-INTERVAL;VALUE=DURATION:PT1H
X-Robots-Tag:noindex
X-PUBLISHED-TTL:PT1H
BEGIN:VTIMEZONE
TZID:UTC
BEGIN:STANDARD
TZOFFSETFROM:+0000
TZOFFSETTO:+0000
TZNAME:UTC
DTSTART:20160101T000000
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
DTSTART;TZID=UTC:20171106T120000
DTEND;TZID=UTC:20171106T130000
DTSTAMP:20260409T024201
CREATED:20180420T135314Z
LAST-MODIFIED:20180420T135314Z
UID:1811-1509969600-1509973200@wp.doc.ic.ac.uk
SUMMARY:HiPEDS Seminar: How can you trust formally verified software?
DESCRIPTION:Abstract: \nFormal verification of software has finally started to become viable: we have examples of formally verified microkernels\, realistic compilers\, hypervisors 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 number of assumptions about the Trusted Computing Base that the software depends 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 take in answering that question for one of the major dependencies: the hardware your software runs on. I will describe the combination of formal verification 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. \nBio: \nAlastair Reid is a Senior Principal Research Engineer at ARM Ltd. His current research focus is on formalizing the ARM architecture specifications and finding ways that those specifications can be used to make hardware and software better. He has 17 granted patents in Computer Architecture and has published over a dozen research papers in Formal Verification\, Software Defined Radio\, Operating Systems\, and Lazy Functional Programming. Before ARM\, he worked/studied at University of Utah\, Yale University\, University of Glasgow and the University of Strathclyde. In his spare time\, he builds his own keyboards and enjoys trashing his body in cyclocross races. You can find him at https://alastairreid.github.io and at @alastair_d_reid.
URL:https://wp.doc.ic.ac.uk/hipeds/event/hipeds-seminar-how-can-you-trust-formally-verified-software/
LOCATION:611 (Gabor Seminar Room)\, EEE Building
ORGANIZER;CN="Giannis Evagorou":MAILTO:g.evagorou15@imperial.ac.uk
END:VEVENT
END:VCALENDAR