![[Search]](/static/images/search.gif){kind=small}
![[A-Z Index]](/static/images/az.gif){kind=small}
![[Contact]](/static/images/contact.gif){kind=small}
![[University of Cambridge]](/static/images/identifier2.gif){kind=small}
![[Talks.cam]](/static/images/talkslogosmall.gif)
Peter Sewell (University of Cambridge)
Thursday 07 July 2022, 13:30-14:30
Wrestling with real systems
- 👤 Speaker: Peter Sewell (University of Cambridge)
- 📅 Date & Time: Thursday 07 July 2022, 13:30 - 14:30
- 📍 Venue: Seminar Room 1, Newton Institute
Abstract
Systems software is often security critical, so a tempting target for verification, but verification needs a trustworthy semantics for the underlying architecture, and verification techniques that can handle it. Neither exist yet, for any major production architecture, so previous work has had to idealise, simplify, or pretend – but we’re getting closer. In this talk I’ll describe recent and ongoing work to establish the pieces of this challenging jigsaw, and start fitting them together and using them, focussing especially on Morello (capability-enabled CHERI -Arm) sequential semantics and security proofs, and on Arm-A sequential and relaxed virtual-memory concurrent semantics and reasoning. I’ll mention some pros and cons of wrestling with real-world architecture.
Series This talk is part of the Isaac Newton Institute Seminar Series series.
Included in Lists
- All CMS events
- bld31
- dh539
- Featured lists
- INI info aggregator
- Isaac Newton Institute Seminar Series
- School of Physical Sciences
- Seminar Room 1, Newton Institute
Note: Ex-directory lists are not shown.