Viðburðir eftir árum

Virtual Computer Science joint ICE-TCS/GSSI seminars: Helgi Kristvin Sigurbjarnarson

Push-Button Verification of Systems Software

  • 22.6.2020, 16:00 - 17:00


Schedule: 22 June, 16:00 GMT/17:00 BST/18:00 Italian time
Virtual link:
Speaker: Helgi Kristvin Sigurbjarnarson (Synthetic Minds, Seattle, USA;
Title: Push-Button Verification of Systems Software

Abstract: Systems software interfaces with hardware, multiplexes resources, and provides common abstractions for modern applications to build on. The correctness and reliability of these systems are critical for the applications and users that depend on them. While formal verification of systems software can be effective at eliminating bugs, it is a non-trivial task, requiring developers to write many lines of proof code for every line of implementation code. This is a considerable engineering effort that requires a high degree of expertise to achieve.
In this talk, which is based on work presented in my doctoral dissertation defended last February, I will present a new approach to designing, specifying, implementing, and verifying systems software in a push-button fashion. By co-designing systems software with automation, I argue it is possible to build correct and reliable systems with substantially less effort. I developed four systems to demonstrate the effectiveness of this approach, using the Z3 satisfiability modulo theories (SMT) solver:
- Yggdrasil, a toolkit for writing file systems,
- an OS kernel named Hyperkernel, which has a high degree of proof automation and low proof burden,
- Nickel, a framework that helps developers design and verify information flow control systems by systematically eliminating covert channels inherent in the interface, and
- Ratatoskr, showing the feasibility of applying push-button verification to distributed protocols.

I argue that these contributions demonstrate the effectiveness of treating automation as a first-class design principle, letting developers build verified systems software with substantially less effort.
Seminars Computer Science
Gran Sasso Science Institute (GSSI), L’Aquila, Italy


Vinsamlegast athugið að á viðburðum Háskólans í Reykjavík (HR) eru teknar ljósmyndir og myndbönd sem notuð eru í markaðsstarfi HR. Hægt er að nálgast frekari upplýsingar á eða með því að senda tölvupóst á netfangið:
Please note that at events hosted at Reykjavik University (RU), photographs and videos are taken which might be used for RU marketing purposes. Read more about this on our or send an e-mail: