[Club2] Einladung: Testing the Red-Black Tree Implementation of the Linux Ke... - Mi 29. Sep. 2021 14:00 - 14:30 (MESZ) (club2 at mailbroy.informatik.tu-muenchen.de)

[piller at in.tum.de]

Sie wurden zum folgenden Termin eingeladen.

Titel: Testing the Red-Black Tree Implementation of the Linux Kernel  
against a Verified Isabelle/HOL Variant
Speaker: Mete PolatType: Bachelor's Thesis Presentation Abstract: In  
this presentation, I show how to construct evidence of correctness forthe  
Red-Black tree (RBT) implementation of the Linux kernel through  
 testing and formal verification. I describe howto expose internal  
 Kernel APIs like itsRBT library to userspace, and how this makes it  
 possible to verify the results of kernel RBToperations by comparing  
them against the ones of a Isabelle/HOL RBT variant.  Moreover, I show  
how identifying new invariants allowed me to prove the correctnessof the  
kernel RBT insert algorithm in Isabelle/HOL.
Wann: Mi 29. Sep. 2021 14:00 – 14:30 Mitteleuropäische Zeit - Berlin
Wo: https://tinyurl.com/ls21coffee
Kalender: club2 at mailbroy.informatik.tu-muenchen.de
Wer
     * piller at in.tum.de- Veranstalter
     * mete.polat at cs.tum.edu
     * club2 at mailbroy.informatik.tu-muenchen.de
     * lukas.bulwahn at gmail.com

Termininformationen:  
https://calendar.google.com/calendar/event?action=VIEW&eid=M25pZTFicnI1bHAzc29mYXE2ZGxrYXRoazEgY2x1YjJAbWFpbGJyb3kuaW5mb3JtYXRpay50dS1tdWVuY2hlbi5kZQ&tok=NTIjc2U2ZWJlM3RvZmY0Y2g1bm11bmlibTVtOThAZ3JvdXAuY2FsZW5kYXIuZ29vZ2xlLmNvbTQzYWUzNTUwMDI5MTlmNDU2ZmRmODliMjkxODk2Mjg1MTA3YTY3OTU&ctz=Europe%2FBerlin&hl=de&es=0

Einladung von Google Kalender: https://calendar.google.com/calendar/

Sie erhalten diese E-Mail unter club2 at mailbroy.informatik.tu-muenchen.de,  
da Sie ein Gast bei diesem Termin sind.

Lehnen Sie diesen Termin ab, um keine weiteren Informationen zu diesem  
Termin zu erhalten. Sie können auch unter  
https://calendar.google.com/calendar/ ein Google-Konto erstellen und Ihre  
Benachrichtigungseinstellungen für Ihren gesamten Kalender steuern.

Wenn Sie diese Einladung weiterleiten, kann jeder Empfänger eine Antwort an  
den Organisator senden und zur Gästeliste hinzugefügt werden. Außerdem  
könnte er weitere Nutzer einladen und Ihre Antwort ändern. Weitere  
Informationen: https://support.google.com/calendar/answer/37135#forwarding
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/club2/attachments/20210902/fd442074/attachment.htm>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: text/calendar
Size: 2461 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/club2/attachments/20210902/fd442074/attachment.ics>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: invite.ics
Type: application/ics
Size: 2511 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/club2/attachments/20210902/fd442074/attachment.bin>