[Club2] Aktualisierte Einladung: A Verified Imperative Implementation of B-Trees - Mi 3. Mär. 2021 03:00 - 03:30 (MEZ) (club2 at mailbroy.informatik.tu-muenchen.de)

[piller at in.tum.de]

Dieser Termin wurde geändert.

Titel: A Verified Imperative Implementation of B-Trees
Speaker: Nils Mündler

Type: Bachelor's Thesis Presentation

Abstract: In this thesis, we use the interactive theorem prover       
Isabelle/HOL to verify an imperative implementation of the classical  
B-tree      data structure.The implementation supports set membership and  
insertion queries with efficient binary search for intra-node navigation.  
This is accomplished by first specifying the structure abstractly in the  
functional modeling language HOL and proving functional      correctness.  
Using manual refinement, we derive an imperative implementation in  
Imperative/HOL. We show the validity of this refinement using the  
separation logic utilities from the Isabelle Refinement Framework.The code  
can be exported to the programming languages SML and      Scala. We examine  
the runtime of all operations indirectly by reproducing      results of the  
logarithmic relationship between height and the number of      nodes.  
Considering development time and lines of code, our approach compares well  
to other approaches at mechanized verifications of the B-tree data  
structure. (geändert)
Wann: Mi 3. Mär. 2021 03:00 – 03: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
     * club2 at mailbroy.informatik.tu-muenchen.de
     * n.muendler at posteo.net

Termininformationen:  
https://calendar.google.com/calendar/event?action=VIEW&eid=N21ldnJsNTk4aDRnMmg4ZHBoa2dnOXZ2Z20gY2x1YjJAbWFpbGJyb3kuaW5mb3JtYXRpay50dS1tdWVuY2hlbi5kZQ&tok=NTIjc2U2ZWJlM3RvZmY0Y2g1bm11bmlibTVtOThAZ3JvdXAuY2FsZW5kYXIuZ29vZ2xlLmNvbWQ5MDJjYzdkOWM1YzdhOTg5MDAzODEwYmU1OTc0NWYzYmViMTkwMjg&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/20210222/47b74b0f/attachment-0001.htm>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: text/calendar
Size: 2665 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/club2/attachments/20210222/47b74b0f/attachment-0001.ics>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: invite.ics
Type: application/ics
Size: 2716 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/club2/attachments/20210222/47b74b0f/attachment-0001.bin>